import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdvancedAdditionWorld.Level11 -- add_right_eq_zero
namespace MyNat
open MyNat

Inequality world.

Level 8: succ_le_succ

Another straightforward one.

Lemma : succ_le_succ

For all naturals a and b, if a ≤ b, then succ a ≤ succ b.

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

Next up Level 9