import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level6 -- add_right_comm
import AdvancedAdditionWorld.Level1 --  succ_inj
namespace MyNat
open MyNat

Inequality world.

Level 12: le_of_succ_le_succ

Lemma : le_of_succ_le_succ

For all naturals a and b, succ a ≤ succ b ⟹ a ≤ b.

theorem 
le_of_succ_le_succ: ∀ (a b : MyNat), succ a ≤ succ b → a ≤ b
le_of_succ_le_succ (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
succ: MyNat → MyNat
succ 
a: MyNat
a ≤ 
succ: MyNat → MyNat
succ 
b: MyNat
b → 
a: MyNat
a ≤ 
b: MyNat
b := by
a, b: MyNat
succ a ≤ succ b → a ≤ b
  intro 
h: succ a ≤ succ b
h
a, b: MyNat
h: succ a ≤ succ b
a ≤ b
  cases 
h: succ a ≤ succ b
h with
a, b: MyNat
h: succ a ≤ succ b
a ≤ b
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
c: MyNat
c 
hc: succ b = succ a + c
hc =>
a, b, c: MyNat
hc: succ b = succ a + c
intro
a ≤ b
    use 
c: MyNat
c
a, b, c: MyNat
hc: succ b = succ a + c
intro
b = a + c
    apply 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj
a, b, c: MyNat
hc: succ b = succ a + c
intro.a
succ b = succ (a + c)
    rw [
a, b, c: MyNat
hc: succ b = succ a + c
intro.a
succ b = succ (a + c)
hc: succ b = succ a + c
hc
a, b, c: MyNat
hc: succ b = succ a + c
intro.a
succ a + c = succ (a + c)]
a, b, c: MyNat
hc: succ b = succ a + c
intro.a
succ a + c = succ (a + c)
    exact 
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add 
a: MyNat
a 
c: MyNat
c
Goals accomplished! 🐙

Next up Level 13