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

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