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

State before:
x : Nat
⊢ x ≤ x
Tactic:
exists zero
State after:
no goals