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

State before:
a : Nat
⊢ a ≤ succ a
Tactic:
exists one
State after:
no goals