no goals
a : Nat
h : a ≠ 0
⊢ 0 < a
match a with
| 0 => contradiction
| a+1 => apply Nat.zero_lt_succ
no goals
a : Nat
h : 0 ≠ 0
⊢ 0 < 0
contradiction
no goals
a✝ a : Nat
h : a + 1 ≠ 0
⊢ 0 < a + 1
apply Nat.zero_lt_succ