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

State before:
a : Nat
h : a ≤ zero
⊢ a = 0
Tactic:
cases h with
| intro w pw =>
  exact add_right_eq_zero (Eq.symm pw)
State after:
no goals

State before:
case intro
a w : Nat
pw : zero = a + w
⊢ a = 0
Tactic:
exact add_right_eq_zero (Eq.symm pw)
State after:
no goals