Theorem: MyNat.succ_ne_zero (TheoremProvingLean/inductive_types.lean)

State before:
a : Nat
⊢ succ a ≠ 0
Tactic:
intro h
State after:
a : Nat
h : succ a = 0
⊢ False

State before:
a : Nat
h : succ a = 0
⊢ False
Tactic:
exact zero_ne_succ a (Eq.symm h)
State after:
no goals