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.Level2 -- le_refl
namespace MyNat
open MyNat

Inequality world.

Level 15: introducing <

To get the remaining collectibles in this world, we need to give a definition of <. By default, the definition of a < b in Lean, once ≤ is defined, is this:

a < b := a ≤ b ∧ ¬ (b ≤ a)

But a much more usable definition would be this:

a < b := succ a ≤ b

Let's prove that these two definitions are the same

Lemma : lt_aux₁

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

lemma 
lt_aux₁: ∀ (a b : MyNat), a ≤ b ∧ ¬b ≤ a → succ a ≤ b
lt_aux₁ (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b ∧ ¬ (
b: MyNat
b ≤ 
a: MyNat
a) → 
succ: MyNat → MyNat
succ 
a: MyNat
a ≤ 
b: MyNat
b := by
a, b: MyNat
a ≤ b ∧ ¬b ≤ a → succ a ≤ b
  intro 
h: a ≤ b ∧ ¬b ≤ a
h
a, b: MyNat
h: a ≤ b ∧ ¬b ≤ a
succ a ≤ b
  cases 
h: a ≤ b ∧ ¬b ≤ a
h with
a, b: MyNat
h: a ≤ b ∧ ¬b ≤ a
succ a ≤ b
  | 
_: ∀ {a b : Prop}, a → b → a ∧ b
_ 
h1: a ≤ b
h1 
h2: ¬b ≤ a
h2 =>
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
intro
succ a ≤ b
    cases 
h1: a ≤ b
h1 with
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
intro
succ a ≤ b
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
c: MyNat
c 
hc: b = a + c
hc =>
a, b: MyNat
h2: ¬b ≤ a
c: MyNat
hc: b = a + c
intro.intro
succ a ≤ b
      cases 
c: MyNat
c with
a, b: MyNat
h2: ¬b ≤ a
c: MyNat
hc: b = a + c
intro.intro
succ a ≤ b
      | 
zero: MyNat
zero =>
a, b: MyNat
h2: ¬b ≤ a
hc: b = a + zero
intro.intro.zero
succ a ≤ b
        exfalso
a, b: MyNat
h2: ¬b ≤ a
hc: b = a + zero
intro.intro.zero.h
False
        rw [
a, b: MyNat
h2: ¬b ≤ a
hc: b = a + zero
intro.intro.zero.h
False
zero_is_0: zero = 0
zero_is_0,
a, b: MyNat
h2: ¬b ≤ a
hc: b = a + 0
intro.intro.zero.h
False 
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
False]
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
False at 
hc: b = a + zero
hc
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
False
        apply 
h2: ¬b ≤ a
h2
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
b ≤ a
        rw [
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
b ≤ a
hc: b = a
hc
a, b: MyNat
h2: ¬b ≤ a
hc: b = a
intro.intro.zero.h
a ≤ a]
Goals accomplished! 🐙
      | 
succ: MyNat → MyNat
succ 
d: MyNat
d =>
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
succ a ≤ b
        use 
d: MyNat
d
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
b = succ a + d
        rw [
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
b = succ a + d
hc: b = a + succ d
hc
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
a + succ d = succ a + d]
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
a + succ d = succ a + d
        rw [
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
a + succ d = succ a + d
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
succ (a + d) = succ a + d]
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
succ (a + d) = succ a + d
        rw [
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
succ (a + d) = succ a + d
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b: MyNat
h2: ¬b ≤ a
d: MyNat
hc: b = a + succ d
intro.intro.succ
succ (a + d) = succ (a + d)]
Goals accomplished! 🐙

Next up Level 16