import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
namespace MyNat
open MyNat

Inequality world.

Level 10: `le_succ_self`

Another simple one.

Lemma : le_succ_self

For all naturals a, a ≤ succ a.

lemma le_succ_self: ∀ (a : MyNat), a ≤ succ a
le_succ_self (a: MyNat
a : MyNat: Type
MyNat) : a: MyNat
a ≤ succ: MyNat → MyNat
succ a: MyNat
a := bya: MyNat
a ≤ succ a
  use 1: MyNat
1Goals accomplished! 🐙

Next up Level 11