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

State before:
m : Nat
⊢ m + zero = m
Tactic:
rfl
State after:
no goals