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

State before:
a : Nat
⊢ zero ≤ a
Tactic:
exists a
State after:
a : Nat
⊢ a = zero + a

State before:
a : Nat
⊢ a = zero + a
Tactic:
rw [zero_add]
State after:
no goals