import MyNat.Definition
import MyNat.Addition -- add_zero
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level2 -- add_assoc
import AdditionWorld.Level3 -- succ_add
import InequalityWorld.Level5 -- le_trans
import InequalityWorld.Level6 -- le_antisymm
import InequalityWorld.Level10 -- le_succ_self
import AdvancedAdditionWorld.Level13 -- ne_succ_self
namespace MyNat
open MyNat

Inequality world.

Level 16: equivalence of two definitions of <

Now let's go the other way.

Lemma : lt_aux₂

For all naturals a and b, succ a ≤ b ⟹ a ≤ b ∧ ¬ (b ≤ a).

lemma 
lt_aux₂: ∀ (a b : MyNat), succ a ≤ b → a ≤ b ∧ ¬b ≤ a
lt_aux₂ (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
succ: MyNat → MyNat
succ 
a: MyNat
a ≤ 
b: MyNat
b → 
a: MyNat
a ≤ 
b: MyNat
b ∧ ¬ (
b: MyNat
b ≤ 
a: MyNat
a) := by
a, b: MyNat
succ a ≤ b → a ≤ b ∧ ¬b ≤ a
  intro 
h: succ a ≤ b
h
a, b: MyNat
h: succ a ≤ b
a ≤ b ∧ ¬b ≤ a
  constructor
a, b: MyNat
h: succ a ≤ b
left
a ≤ b
a, b: MyNat
h: succ a ≤ b
right
¬b ≤ a
  {
a, b: MyNat
h: succ a ≤ b
left
a ≤ b
    apply 
le_trans: ∀ (a b c : MyNat), a ≤ b → b ≤ c → a ≤ c
le_trans 
a: MyNat
a (
succ: MyNat → MyNat
succ 
a: MyNat
a) 
b: MyNat
b
a, b: MyNat
h: succ a ≤ b
left.hab
a ≤ succ a
a, b: MyNat
h: succ a ≤ b
left.hbc
succ a ≤ b
    exact 
le_succ_self: ∀ (a : MyNat), a ≤ succ a
le_succ_self 
a: MyNat
a
a, b: MyNat
h: succ a ≤ b
left.hbc
succ a ≤ b
    exact 
h: succ a ≤ b
h
Goals accomplished! 🐙
  }
a, b: MyNat
h: succ a ≤ b
right
¬b ≤ a
  {
a, b: MyNat
h: succ a ≤ b
right
¬b ≤ a
    intro 
nh: b ≤ a
nh
a, b: MyNat
h: succ a ≤ b
nh: b ≤ a
right
False
    apply 
ne_succ_self: ∀ (n : MyNat), n ≠ succ n
ne_succ_self 
a: MyNat
a
a, b: MyNat
h: succ a ≤ b
nh: b ≤ a
right
a = succ a
    apply 
le_antisymm: ∀ (a b : MyNat), a ≤ b → b ≤ a → a = b
le_antisymm 
a: MyNat
a (
succ: MyNat → MyNat
succ 
a: MyNat
a)
a, b: MyNat
h: succ a ≤ b
nh: b ≤ a
right.hab
a ≤ succ a
a, b: MyNat
h: succ a ≤ b
nh: b ≤ a
right.hba
succ a ≤ a
    exact 
le_succ_self: ∀ (a : MyNat), a ≤ succ a
le_succ_self 
a: MyNat
a
a, b: MyNat
h: succ a ≤ b
nh: b ≤ a
right.hba
succ a ≤ a
    exact 
le_trans: ∀ (a b c : MyNat), a ≤ b → b ≤ c → a ≤ c
le_trans (
succ: MyNat → MyNat
succ 
a: MyNat
a) 
b: MyNat
b 
a: MyNat
a 
h: succ a ≤ b
h 
nh: b ≤ a
nh
Goals accomplished! 🐙
  }
Goals accomplished! 🐙

Now for the payoff.

Next up Level 17