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

Inequality world.

Level 4: `zero_le`

Another easy one.

Lemma : zero_le

For all naturals a, 0 ≤ a.

lemma zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le (a: MyNat
a : MyNat: Type
MyNat) : 0: MyNat
0 ≤ a: MyNat
a := bya: MyNat
0 ≤ a
  use a: MyNat
aa: MyNat
a = 0 + a
  rw [a: MyNat
a = 0 + azero_add: ∀ (n : MyNat), 0 + n = n
zero_adda: MyNat
a = a]Goals accomplished! 🐙

Next up Level 5