import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level2 -- add_assoc
import AdvancedAdditionWorld.Level8 -- eq_zero_of_add_right_eq_self
import AdvancedAdditionWorld.Level11 -- add_right_eq_zero
namespace MyNat
open MyNat

Inequality world.

Level 6: le_antisymm

In Advanced Addition World you proved

eq_zero_of_add_right_eq_self (a b : MyNat) : a + b = a → b = 0.

This might be useful in this level.

Another tip: if you want to create a new hypothesis, you can use the have tactic. For example, if you have a hypothesis hd : a + (c + d) = a and you want a hypothesis h : c + d = 0 then you can write

have h := eq_zero_of_add_right_eq_self hd

Lemma : le_antisymm

≤ is antisymmetric. In other words, if a ≤ b and b ≤ a then a = b.

theorem 
le_antisymm: ∀ (a b : MyNat), a ≤ b → b ≤ a → a = b
le_antisymm (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) (
hab: a ≤ b
hab : 
a: MyNat
a ≤ 
b: MyNat
b) (
hba: b ≤ a
hba : 
b: MyNat
b ≤ 
a: MyNat
a) : 
a: MyNat
a = 
b: MyNat
b := by
a, b: MyNat
hab: a ≤ b
hba: b ≤ a
a = b
  cases 
hab: a ≤ b
hab with
a, b: MyNat
hab: a ≤ b
hba: b ≤ a
a = b
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
c: MyNat
c 
hc: b = a + c
hc =>
a, b: MyNat
hba: b ≤ a
c: MyNat
hc: b = a + c
intro
a = b
    cases 
hba: b ≤ a
hba with
a, b: MyNat
hba: b ≤ a
c: MyNat
hc: b = a + c
intro
a = b
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
d: MyNat
d 
hd: a = b + d
hd =>
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = b + d
intro.intro
a = b
      rw [
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = b + d
intro.intro
a = b
hc: b = a + c
hc,
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = a + c + d
intro.intro
a = b 
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_assoc
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = a + (c + d)
intro.intro
a = b]
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = a + (c + d)
intro.intro
a = b at 
hd: a = b + d
hd
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd: a = a + (c + d)
intro.intro
a = b
      have 
hd: a + (c + d) = a
hd := 
hd: a = a + (c + d)
hd.
symm: ∀ {α : Type} {a b : α}, a = b → b = a
symm
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
intro.intro
a = b
      have 
h: c + d = 0
h := 
eq_zero_of_add_right_eq_self: ∀ {a b : MyNat}, a + b = a → b = 0
eq_zero_of_add_right_eq_self 
hd: a + (c + d) = a
hd
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
intro.intro
a = b
      have 
h2: c = 0
h2 := 
add_right_eq_zero: ∀ {a b : MyNat}, a + b = 0 → a = 0
add_right_eq_zero 
h: c + d = 0
h
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b
      rw [
a, b, c: MyNat
hc: b = a + c
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b
h2: c = 0
h2
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b]
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b at 
hc: b = a + c
hc
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b
      rw [
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = b
hc: b = a + 0
hc
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = a + 0]
a, b, c: MyNat
hc: b = a + 0
d: MyNat
hd✝: a = a + (c + d)
hd: a + (c + d) = a
h: c + d = 0
h2: c = 0
intro.intro
a = a + 0
      exact 
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero 
a: MyNat
a
Goals accomplished! 🐙

This proved that the natural numbers are a partial order!

-- BUGBUG : collectibles
-- instance : partial_order MyNat := by structure_helper

Next up Level 7