import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import AdvancedAdditionWorld.Level11 -- add_right_eq_zero
import Mathlib.Tactic.LeftRight
import InequalityWorld.Level4 -- zero_le
import InequalityWorld.Level8 -- succ_le_succ
namespace MyNat
open MyNat

Inequality world.

Level 9: le_total

Lemma : le_total

For all naturals a and b, either a ≤ b or b ≤ a.

theorem 
le_total: ∀ (a b : MyNat), a ≤ b ∨ b ≤ a
le_total (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b ∨ 
b: MyNat
b ≤ 
a: MyNat
a := by
a, b: MyNat
a ≤ b ∨ b ≤ a
  revert 
a: MyNat
a
b: MyNat
∀ (a : MyNat), a ≤ b ∨ b ≤ a
  induction 
b: MyNat
b with
b: MyNat
∀ (a : MyNat), a ≤ b ∨ b ≤ a
  | 
zero: MyNat
zero =>
zero
∀ (a : MyNat), a ≤ zero ∨ zero ≤ a
    intro 
a: MyNat
a
a: MyNat
zero
a ≤ zero ∨ zero ≤ a
    right
a: MyNat
zero.h
zero ≤ a
    exact 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le 
a: MyNat
a
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
d: MyNat
d 
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
hd =>
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
succ
∀ (a : MyNat), a ≤ succ d ∨ succ d ≤ a
    intro 
a: MyNat
a
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
succ
a ≤ succ d ∨ succ d ≤ a
    cases 
a: MyNat
a with
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
succ
a ≤ succ d ∨ succ d ≤ a
    | 
zero: MyNat
zero =>
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
succ.zero
zero ≤ succ d ∨ succ d ≤ zero
      left
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
succ.zero.h
zero ≤ succ d
      exact 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le 
_: MyNat
_
Goals accomplished! 🐙
    | 
succ: MyNat → MyNat
succ 
a: MyNat
a =>
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
succ.succ
succ a ≤ succ d ∨ succ d ≤ succ a
      have 
h2: a ≤ d ∨ d ≤ a
h2 := 
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
hd 
a: MyNat
a
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h2: a ≤ d ∨ d ≤ a
succ.succ
succ a ≤ succ d ∨ succ d ≤ succ a
      cases 
h2: a ≤ d ∨ d ≤ a
h2 with
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h2: a ≤ d ∨ d ≤ a
succ.succ
succ a ≤ succ d ∨ succ d ≤ succ a
      | 
inl: ∀ {a b : Prop}, a → a ∨ b
inl 
h: a ≤ d
h =>
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h: a ≤ d
succ.succ.inl
succ a ≤ succ d ∨ succ d ≤ succ a
        left
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h: a ≤ d
succ.succ.inl.h
succ a ≤ succ d
        exact 
succ_le_succ: ∀ (a b : MyNat), a ≤ b → succ a ≤ succ b
succ_le_succ 
a: MyNat
a 
d: MyNat
d 
h: a ≤ d
h
Goals accomplished! 🐙
      | 
inr: ∀ {a b : Prop}, b → a ∨ b
inr 
h: d ≤ a
h =>
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h: d ≤ a
succ.succ.inr
succ a ≤ succ d ∨ succ d ≤ succ a
        right
d: MyNat
hd: ∀ (a : MyNat), a ≤ d ∨ d ≤ a
a: MyNat
h: d ≤ a
succ.succ.inr.h
succ d ≤ succ a
        exact 
succ_le_succ: ∀ (a b : MyNat), a ≤ b → succ a ≤ succ b
succ_le_succ 
d: MyNat
d 
a: MyNat
a 
h: d ≤ a
h
Goals accomplished! 🐙

See the revert tactic

Note in the above proof that exact succ_le_succ a d h is just shorthand for: apply succ_le_succ a d exact h

Another collectible: the naturals are a linear order.

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

Next up Level 10