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

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