Theorem: LoVe.Nat.le_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.le_of_succ_le_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_le_succ }
State after:
no goals

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

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