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

State before:
a b : Nat
hs : succ (succ a) = succ (succ b)
⊢ a = b
Tactic:
exact succ_inj (succ_inj hs)
State after:
no goals