import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import AdvancedAdditionWorld.Level11 -- add_right_eq_zero
namespace MyNat
open MyNat

Inequality world

Level 7: `le_zero`

We proved add_right_eq_zero back in advanced addition world. Remember that you can do things like have h2 := add_right_eq_zero h1 if h1 : a + c = 0.

Lemma : le_zero

For all naturals a, if a ≤ 0 then a = 0.

lemma le_zero: ∀ (a : MyNat), a ≤ 0 → a = 0
le_zero (a: MyNat
a : MyNat: Type
MyNat) (h: a ≤ 0
h : a: MyNat
a ≤ 0: MyNat
0) : a: MyNat
a = 0: MyNat
0 := bya: MyNat
h: a ≤ 0
a = 0
  cases h: a ≤ 0
h witha: MyNat
h: a ≤ 0
a = 0
  | _: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ c: MyNat
c hc: 0 = a + c
hc =>a, c: MyNat
hc: 0 = a + c
introa = 0
    have hc: a + c = 0
hc := hc: 0 = a + c
hc.symm: ∀ {α : Type} {a b : α}, a = b → b = a
symma, c: MyNat
hc✝: 0 = a + c
hc: a + c = 0
introa = 0
    exact add_right_eq_zero: ∀ {a b : MyNat}, a + b = 0 → a = 0
add_right_eq_zero hc: a + c = 0
hcGoals accomplished! 🐙

Next up Level 8