no goals
b : Nat
x✝ : 0 < succ b
⊢ succ b - 0 ≠ 0
simp
a b : Nat
h : succ a < succ b
⊢ b - a ≠ 0
a b : Nat
h : succ a < succ b
⊢ succ b - succ a ≠ 0
rw [Nat.succ_sub_succ]
no goals
a b : Nat
h : succ a < succ b
⊢ b - a ≠ 0
exact sub_ne_zero_of_lt (Nat.lt_of_succ_lt_succ h)