import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level2 -- add_assoc
namespace MyNat
open MyNat

Inequality world.

Level 14: add_le_add_left

I know these are easy and we've done several already, but this is one of the axioms for an ordered commutative monoid! The nature of formalizing is that we should formalize all "obvious" lemmas, and then when we're actually using ≤ in real life, everything will be there. Note also, of course, that all of these lemmas are already formalized in Lean's maths library already, for Lean's inbuilt natural numbers.

Lemma : add_le_add_left

If a ≤ b then for all t, t+a ≤ t+b.

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

Next up Level 15