Theorem: LoVe.Nat.lt_succ (LoVe/LoVelib.lean)

State before:
m n : ℕ
⊢ Nat.succ m < Nat.succ n ↔ m < n
Tactic:
apply Iff.intro
State after:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n

case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n

State before:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n

case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
{ apply Nat.lt_of_succ_lt_succ }
State after:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n

State before:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
{ apply Nat.succ_lt_succ }
State after:
no goals

State before:
case mp
m n : ℕ
⊢ Nat.succ m < Nat.succ n → m < n
Tactic:
apply Nat.lt_of_succ_lt_succ
State after:
no goals

State before:
case mpr
m n : ℕ
⊢ m < n → Nat.succ m < Nat.succ n
Tactic:
apply Nat.succ_lt_succ
State after:
no goals