import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level2 -- add_assoc
import InequalityWorld.Level2 -- le_refl_mynat
import Mathlib.Init.Algebra.Order
namespace MyNat
open MyNat

Inequality world.

Level 5: le_trans

Another straightforward one.

Lemma : le_trans

≤ is transitive. In other words, if a ≤ b and b ≤ c then a ≤ c.

theorem 
le_trans: ∀ (a b c : MyNat), a ≤ b → b ≤ c → a ≤ c
le_trans (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) (
hab: a ≤ b
hab : 
a: MyNat
a ≤ 
b: MyNat
b) (
hbc: b ≤ c
hbc : 
b: MyNat
b ≤ 
c: MyNat
c) : 
a: MyNat
a ≤ 
c: MyNat
c := by
a, b, c: MyNat
hab: a ≤ b
hbc: b ≤ c
a ≤ c
  cases 
hab: a ≤ b
hab with
a, b, c: MyNat
hab: a ≤ b
hbc: b ≤ c
a ≤ c
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
d: MyNat
d 
hd: b = a + d
hd =>
a, b, c: MyNat
hbc: b ≤ c
d: MyNat
hd: b = a + d
intro
a ≤ c
    cases 
hbc: b ≤ c
hbc with
a, b, c: MyNat
hbc: b ≤ c
d: MyNat
hd: b = a + d
intro
a ≤ c
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
e: MyNat
e 
he: c = b + e
he =>
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
a ≤ c
      use (
d: MyNat
d + 
e: MyNat
e)
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = a + (d + e)
      rw [
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = a + (d + e)←
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_assoc
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = a + d + e]
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = a + d + e
      rw [
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = a + d + e←
hd: b = a + d
hd
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = b + e]
a, b, c, d: MyNat
hd: b = a + d
e: MyNat
he: c = b + e
intro.intro
c = b + e
      assumption
Goals accomplished! 🐙

This proved that the natural numbers are a preorder.

instance: Preorder MyNat
instance : 
Preorder: Type → Type
Preorder 
MyNat: Type
MyNat :=
  ⟨
le_refl_mynat: ∀ (x : MyNat), x ≤ x
le_refl_mynat, 
le_trans: ∀ (a b c : MyNat), a ≤ b → b ≤ c → a ≤ c
le_trans, 
lt: ∀ (a b : MyNat), a < b ↔ a ≤ b ∧ ¬b ≤ a
lt⟩

Next up Level 6