Theorem: nat_succ_gt_succ (Katydid/Std/Lists.lean)

State before:
n m : ℕ
⊢ succ n > succ m → n > m
Tactic:
intro h
State after:
n m : ℕ
h : succ n > succ m
⊢ n > m

State before:
n m : ℕ
h : succ n > succ m
⊢ n > m
Tactic:
cases h with
| refl =>
  constructor
| step s =>
  apply Nat.le_of_succ_le_succ
  exact (Nat.le_succ_of_le s)
State after:
no goals

State before:
case refl
m : ℕ
⊢ succ m > m
Tactic:
constructor
State after:
no goals

State before:
case step
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ n > m
Tactic:
apply Nat.le_of_succ_le_succ
State after:
case step.a
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ succ (succ m) ≤ succ n

State before:
case step.a
n m : ℕ
s : Nat.le (succ (succ m)) n
⊢ succ (succ m) ≤ succ n
Tactic:
exact (Nat.le_succ_of_le s)
State after:
no goals