The Lean Natural Numbers

import MyNat.Definition
import MyNat.Power
import MyNat.Inequality -- LE
import InequalityWorld.Level4 -- zero_le
import InequalityWorld.Level5 -- le_trans
import InequalityWorld.Level17 -- lt, lt_iff_succ_le
import MultiplicationWorld.Level4 -- mul_add
import MultiplicationWorld.Level8 -- mul_comm
namespace MyNat
open MyNat

lemma 
lt_irrefl: ∀ (a : MyNat), ¬a < a
lt_irrefl (
a: MyNat
a : 
MyNat: Type
MyNat) : ¬ (
a: MyNat
a < 
a: MyNat
a) := by
a: MyNat
¬a < a
  intro 
h: a < a
h
a: MyNat
h: a < a
False
  cases 
h: a < a
h with
a: MyNat
h: a < a
False
  | 
_: ∀ {a b : Prop}, a → b → a ∧ b
_ 
h1: a ≤ a
h1 
h2: ¬a ≤ a
h2 =>
a: MyNat
h1: a ≤ a
h2: ¬a ≤ a
intro
False
    apply 
h2: ¬a ≤ a
h2
a: MyNat
h1: a ≤ a
h2: ¬a ≤ a
intro
a ≤ a
    exact 
h1: a ≤ a
h1
Goals accomplished! 🐙

lemma 
ne_of_lt: ∀ (a b : MyNat), a < b → a ≠ b
ne_of_lt (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → 
a: MyNat
a ≠ 
b: MyNat
b := by
a, b: MyNat
a < b → a ≠ b
  intro 
h: a < b
h
a, b: MyNat
h: a < b
a ≠ b
  intro 
h1: a = b
h1
a, b: MyNat
h: a < b
h1: a = b
False
  cases 
h: a < b
h with
a, b: MyNat
h: a < b
h1: a = b
False
  | 
_: ∀ {a b : Prop}, a → b → a ∧ b
_ 
h2: a ≤ b
h2 
h3: ¬b ≤ a
h3 =>
a, b: MyNat
h1: a = b
h2: a ≤ b
h3: ¬b ≤ a
intro
False
    apply 
h3: ¬b ≤ a
h3
a, b: MyNat
h1: a = b
h2: a ≤ b
h3: ¬b ≤ a
intro
b ≤ a
    rw [
a, b: MyNat
h1: a = b
h2: a ≤ b
h3: ¬b ≤ a
intro
b ≤ a
h1: a = b
h1
a, b: MyNat
h1: a = b
h2: a ≤ b
h3: ¬b ≤ a
intro
b ≤ b]
Goals accomplished! 🐙

theorem 
not_lt_zero: ∀ (a : MyNat), ¬a < 0
not_lt_zero (
a: MyNat
a : 
MyNat: Type
MyNat) : ¬(
a: MyNat
a < 
0: MyNat
0) := by
a: MyNat
¬a < 0
  intro 
h: a < 0
h
a: MyNat
h: a < 0
False
  cases 
h: a < 0
h with
a: MyNat
h: a < 0
False
  | 
_: ∀ {a b : Prop}, a → b → a ∧ b
_ 
ha: a ≤ 0
ha 
hna: ¬0 ≤ a
hna =>
a: MyNat
ha: a ≤ 0
hna: ¬0 ≤ a
intro
False
    apply 
hna: ¬0 ≤ a
hna
a: MyNat
ha: a ≤ 0
hna: ¬0 ≤ a
intro
0 ≤ a
    exact 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le 
a: MyNat
a
Goals accomplished! 🐙

theorem 
lt_of_lt_of_le: ∀ (a b c : MyNat), a < b → b ≤ c → a < c
lt_of_lt_of_le (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → 
b: MyNat
b ≤ 
c: MyNat
c → 
a: MyNat
a < 
c: MyNat
c := by
a, b, c: MyNat
a < b → b ≤ c → a < c
  intro 
hab: a < b
hab
a, b, c: MyNat
hab: a < b
b ≤ c → a < c
  intro 
hbc: b ≤ c
hbc
a, b, c: MyNat
hab: a < b
hbc: b ≤ c
a < c
  rw [
a, b, c: MyNat
hab: a < b
hbc: b ≤ c
a < c
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b, c: MyNat
hab: succ a ≤ b
hbc: b ≤ c
succ a ≤ c]
a, b, c: MyNat
hab: succ a ≤ b
hbc: b ≤ c
succ a ≤ c at 
hab: a < b
hab ⊢
a, b, c: MyNat
hab: succ a ≤ b
hbc: b ≤ c
succ a ≤ c
  cases 
hbc: b ≤ c
hbc with
a, b, c: MyNat
hab: succ a ≤ b
hbc: b ≤ c
succ a ≤ c
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
x: MyNat
x 
hx: c = b + x
hx =>
a, b, c: MyNat
hab: succ a ≤ b
x: MyNat
hx: c = b + x
intro
succ a ≤ c
    cases 
hab: succ a ≤ b
hab with
a, b, c: MyNat
hab: succ a ≤ b
x: MyNat
hx: c = b + x
intro
succ a ≤ c
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
y: MyNat
y 
hy: b = succ a + y
hy =>
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ c
      rw [
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ c
hx: c = b + x
hx
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ b + x]
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ b + x
      rw [
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ b + x
hy: b = succ a + y
hy
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ a + y + x]
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ a + y + x
      use 
y: MyNat
y + 
x: MyNat
x
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a + y + x = succ a + (y + x)
      rw [
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a + y + x = succ a + (y + x)
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_assoc
a, b, c, x: MyNat
hx: c = b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a + (y + x) = succ a + (y + x)]
Goals accomplished! 🐙

theorem 
lt_of_le_of_lt: ∀ (a b c : MyNat), a ≤ b → b < c → a < c
lt_of_le_of_lt (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b → 
b: MyNat
b < 
c: MyNat
c → 
a: MyNat
a < 
c: MyNat
c := by
a, b, c: MyNat
a ≤ b → b < c → a < c
  intro 
hab: a ≤ b
hab
a, b, c: MyNat
hab: a ≤ b
b < c → a < c
  intro 
hbc: b < c
hbc
a, b, c: MyNat
hab: a ≤ b
hbc: b < c
a < c
  rw [
a, b, c: MyNat
hab: a ≤ b
hbc: b < c
a < c
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b, c: MyNat
hab: a ≤ b
hbc: succ b ≤ c
succ a ≤ c]
a, b, c: MyNat
hab: a ≤ b
hbc: succ b ≤ c
succ a ≤ c at 
hbc: b < c
hbc ⊢
a, b, c: MyNat
hab: a ≤ b
hbc: succ b ≤ c
succ a ≤ c
  cases 
hbc: succ b ≤ c
hbc with
a, b, c: MyNat
hab: a ≤ b
hbc: succ b ≤ c
succ a ≤ c
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
x: MyNat
x 
hx: c = succ b + x
hx =>
a, b, c: MyNat
hab: a ≤ b
x: MyNat
hx: c = succ b + x
intro
succ a ≤ c
    cases 
hab: a ≤ b
hab with
a, b, c: MyNat
hab: a ≤ b
x: MyNat
hx: c = succ b + x
intro
succ a ≤ c
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
y: MyNat
y 
hy: b = a + y
hy =>
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ c
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ c
hx: c = succ b + x
hx
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ succ b + x]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ succ b + x
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ succ b + x
hy: b = a + y
hy
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ succ (a + y) + x]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ a ≤ succ (a + y) + x
      use 
y: MyNat
y + 
x: MyNat
x
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y) + x = succ a + (y + x)
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y) + x = succ a + (y + x)
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ a + (y + x)]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ a + (y + x)
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ a + (y + x)
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ (a + (y + x))]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ (a + (y + x))
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + y + x) = succ (a + (y + x))
add_assoc: ∀ (a b c : MyNat), a + b + c = a + (b + c)
add_assoc
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = a + y
intro.intro
succ (a + (y + x)) = succ (a + (y + x))]
Goals accomplished! 🐙

theorem 
lt_trans: ∀ (a b c : MyNat), a < b → b < c → a < c
lt_trans (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → 
b: MyNat
b < 
c: MyNat
c → 
a: MyNat
a < 
c: MyNat
c := by
a, b, c: MyNat
a < b → b < c → a < c
  intro 
hab: a < b
hab
a, b, c: MyNat
hab: a < b
b < c → a < c
  intro 
hbc: b < c
hbc
a, b, c: MyNat
hab: a < b
hbc: b < c
a < c
  rw [
a, b, c: MyNat
hab: a < b
hbc: b < c
a < c
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b, c: MyNat
hab: succ a ≤ b
hbc: succ b ≤ c
succ a ≤ c]
a, b, c: MyNat
hab: succ a ≤ b
hbc: succ b ≤ c
succ a ≤ c at 
hab: a < b
hab 
hbc: b < c
hbc ⊢
a, b, c: MyNat
hab: succ a ≤ b
hbc: succ b ≤ c
succ a ≤ c
  cases 
hbc: succ b ≤ c
hbc with
a, b, c: MyNat
hab: succ a ≤ b
hbc: succ b ≤ c
succ a ≤ c
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
x: MyNat
x 
hx: c = succ b + x
hx =>
a, b, c: MyNat
hab: succ a ≤ b
x: MyNat
hx: c = succ b + x
intro
succ a ≤ c
    cases 
hab: succ a ≤ b
hab with
a, b, c: MyNat
hab: succ a ≤ b
x: MyNat
hx: c = succ b + x
intro
succ a ≤ c
    | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
y: MyNat
y 
hy: b = succ a + y
hy =>
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ c
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ c
hx: c = succ b + x
hx
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ b + x]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ b + x
      rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ b + x
hy: b = succ a + y
hy
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ (succ a + y) + x]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ a ≤ succ (succ a + y) + x
      use 
y: MyNat
y + 
x: MyNat
x + 
1: MyNat
1
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ a + y) + x = succ a + (y + x + 1)
      repeat
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ a + y) + x = succ a + (y + x + 1) rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ a + y + x) = succ a + (y + x + 1)
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ (a + y) + x) = succ a + (y + x + 1)]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ (a + y + x)) = succ (a + (y + x + 1))
      repeat
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
succ (succ (a + y + x)) = succ (a + (y + x + 1)) rw [
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
a + y + x + 1 + 1 = a + (y + x + 1) + 1
succ_eq_add_one: ∀ (n : MyNat), succ n = n + 1
succ_eq_add_one
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
a + y + x + 1 + 1 = a + (y + x + 1) + 1]
a, b, c, x: MyNat
hx: c = succ b + x
y: MyNat
hy: b = succ a + y
intro.intro
a + y + x + 1 + 1 = succ (a + (y + x + 1))
      simp
Goals accomplished! 🐙

theorem 
lt_iff_le_and_ne: ∀ (a b : MyNat), a < b ↔ a ≤ b ∧ a ≠ b
lt_iff_le_and_ne (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b ↔ 
a: MyNat
a ≤ 
b: MyNat
b ∧ 
a: MyNat
a ≠ 
b: MyNat
b := by
a, b: MyNat
a < b ↔ a ≤ b ∧ a ≠ b
  constructor
a, b: MyNat
mp
a < b → a ≤ b ∧ a ≠ b
a, b: MyNat
mpr
a ≤ b ∧ a ≠ b → a < b
  {
a, b: MyNat
mp
a < b → a ≤ b ∧ a ≠ b
    intro 
h: a < b
h
a, b: MyNat
h: a < b
mp
a ≤ b ∧ a ≠ b
    cases 
h: a < b
h with
a, b: MyNat
h: a < b
mp
a ≤ b ∧ 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
mp.intro
a ≤ b ∧ a ≠ b
      constructor
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
mp.intro.left
a ≤ b
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
mp.intro.right
a ≠ b
      assumption
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
mp.intro.right
a ≠ b
      intro 
h: a = b
h
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
h: a = b
mp.intro.right
False
      apply 
h2: ¬b ≤ a
h2
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
h: a = b
mp.intro.right
b ≤ a
      rw [
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
h: a = b
mp.intro.right
b ≤ a
h: a = b
h
a, b: MyNat
h1: a ≤ b
h2: ¬b ≤ a
h: a = b
mp.intro.right
b ≤ b]
Goals accomplished! 🐙
  }
a, b: MyNat
mpr
a ≤ b ∧ a ≠ b → a < b
  {
a, b: MyNat
mpr
a ≤ b ∧ a ≠ b → a < b
    intro 
h: a ≤ b ∧ a ≠ b
h
a, b: MyNat
h: a ≤ b ∧ a ≠ b
mpr
a < b
    cases 
h: a ≤ b ∧ a ≠ b
h with
a, b: MyNat
h: a ≤ b ∧ a ≠ b
mpr
a < b
    | 
_: ∀ {a b : Prop}, a → b → a ∧ b
_ 
h1: a ≤ b
h1 
h2: a ≠ b
h2 =>
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
mpr.intro
a < b
    constructor
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
mpr.intro.left
a ≤ b
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
mpr.intro.right
¬b ≤ a
    exact 
h1: a ≤ b
h1
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
mpr.intro.right
¬b ≤ a
    intro 
h: b ≤ a
h
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
h: b ≤ a
mpr.intro.right
False
    apply 
h2: a ≠ b
h2
a, b: MyNat
h1: a ≤ b
h2: a ≠ b
h: b ≤ a
mpr.intro.right
a = b
    exact 
le_antisymm: ∀ (a b : MyNat), a ≤ b → b ≤ a → a = b
le_antisymm 
_: MyNat
_ 
_: MyNat
_ 
h1: a ≤ b
h1 
h: b ≤ a
h
Goals accomplished! 🐙
  }
Goals accomplished! 🐙

theorem 
lt_succ_self: ∀ (n : MyNat), n < succ n
lt_succ_self (
n: MyNat
n : 
MyNat: Type
MyNat) : 
n: MyNat
n < 
succ: MyNat → MyNat
succ 
n: MyNat
n := by
n: MyNat
n < succ n
  rw [
n: MyNat
n < succ n
lt_iff_le_and_ne: ∀ (a b : MyNat), a < b ↔ a ≤ b ∧ a ≠ b
lt_iff_le_and_ne
n: MyNat
n ≤ succ n ∧ n ≠ succ n]
n: MyNat
n ≤ succ n ∧ n ≠ succ n
  constructor
n: MyNat
left
n ≤ succ n
n: MyNat
right
n ≠ succ n
  {
n: MyNat
left
n ≤ succ n
    use 
1: MyNat
1
Goals accomplished! 🐙
  }
n: MyNat
right
n ≠ succ n
  {
n: MyNat
right
n ≠ succ n
    intro 
h: n = succ n
h
n: MyNat
h: n = succ n
right
False
    exact 
ne_succ_self: ∀ (n : MyNat), n ≠ succ n
ne_succ_self 
n: MyNat
n 
h: n = succ n
h
Goals accomplished! 🐙
  }
Goals accomplished! 🐙

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


lemma 
lt_succ_iff_le: ∀ (m n : MyNat), m < succ n ↔ m ≤ n
lt_succ_iff_le (
m: MyNat
m 
n: MyNat
n : 
MyNat: Type
MyNat) : 
m: MyNat
m < 
succ: MyNat → MyNat
succ 
n: MyNat
n ↔ 
m: MyNat
m ≤ 
n: MyNat
n := by
m, n: MyNat
m < succ n ↔ m ≤ n
  rw [
m, n: MyNat
m < succ n ↔ m ≤ n
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
m, n: MyNat
succ m ≤ succ n ↔ m ≤ n]
m, n: MyNat
succ m ≤ succ n ↔ m ≤ n
  exact 
succ_le_succ_iff: ∀ (m n : MyNat), succ m ≤ succ n ↔ m ≤ n
succ_le_succ_iff 
m: MyNat
m 
n: MyNat
n
Goals accomplished! 🐙


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

lemma 
lt_of_add_lt_add_left: ∀ (a b c : MyNat), a + b < a + c → b < c
lt_of_add_lt_add_left (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a + 
b: MyNat
b < 
a: MyNat
a + 
c: MyNat
c → 
b: MyNat
b < 
c: MyNat
c := by
a, b, c: MyNat
a + b < a + c → b < c
  repeat
a, b, c: MyNat
a + b < a + c → b < c rw [
a, b, c: MyNat
succ (a + b) ≤ a + c → b < c
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b, c: MyNat
succ (a + b) ≤ a + c → b < c]
a, b, c: MyNat
succ (a + b) ≤ a + c → b < c
  intro 
h: succ (a + b) ≤ a + c
h
a, b, c: MyNat
h: succ (a + b) ≤ a + c
succ b ≤ c
  apply 
le_of_add_le_add_left: ∀ (a b c : MyNat), a + b ≤ a + c → b ≤ c
le_of_add_le_add_left 
a: MyNat
a
a, b, c: MyNat
h: succ (a + b) ≤ a + c
a
a + succ b ≤ a + c
  rw [
a, b, c: MyNat
h: succ (a + b) ≤ a + c
a
a + succ b ≤ a + c
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, c: MyNat
h: succ (a + b) ≤ a + c
a
succ (a + b) ≤ a + c]
a, b, c: MyNat
h: succ (a + b) ≤ a + c
a
succ (a + b) ≤ a + c
  assumption
Goals accomplished! 🐙

lemma 
add_lt_add_right: ∀ (a b : MyNat), a < b → ∀ (c : MyNat), a + c < b + c
add_lt_add_right (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → ∀ 
c: MyNat
c : 
MyNat: Type
MyNat, 
a: MyNat
a + 
c: MyNat
c < 
b: MyNat
b + 
c: MyNat
c := by
a, b: MyNat
a < b → ∀ (c : MyNat), a + c < b + c
  intro 
h: a < b
h
a, b: MyNat
h: a < b
∀ (c : MyNat), a + c < b + c
  intro 
c: MyNat
c
a, b: MyNat
h: a < b
c: MyNat
a + c < b + c
  rw [
a, b: MyNat
h: a < b
c: MyNat
a + c < b + c
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b: MyNat
h: succ a ≤ b
c: MyNat
succ (a + c) ≤ b + c]
a, b: MyNat
h: succ a ≤ b
c: MyNat
succ (a + c) ≤ b + c at 
h: a < b
h ⊢
a, b: MyNat
h: succ a ≤ b
c: MyNat
succ (a + c) ≤ b + c
  cases 
h: succ a ≤ b
h with
a, b: MyNat
h: succ a ≤ b
c: MyNat
succ (a + c) ≤ b + c
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
d: MyNat
d 
hd: b = succ a + d
hd =>
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ (a + c) ≤ b + c
    use 
d: MyNat
d
a, b, c, d: MyNat
hd: b = succ a + d
intro
b + c = succ (a + c) + d
    rw [
a, b, c, d: MyNat
hd: b = succ a + d
intro
b + c = succ (a + c) + d
hd: b = succ a + d
hd
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ a + d + c = succ (a + c) + d]
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ a + d + c = succ (a + c) + d
    repeat
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ a + d + c = succ (a + c) + d rw [
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ a + d + c = succ (a + c) + d
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ (a + d + c) = succ (a + c + d)]
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ (a + d + c) = succ (a + c) + d
    rw [
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ (a + d + c) = succ (a + c + d)
add_right_comm: ∀ (a b c : MyNat), a + b + c = a + c + b
add_right_comm
a, b, c, d: MyNat
hd: b = succ a + d
intro
succ (a + c + d) = succ (a + c + d)]
Goals accomplished! 🐙

-- BUGBUG: collectibles
-- and now we get three achievements!
-- instance : ordered_comm_monoid MyNat :=
-- { add_le_add_left := λ _ _, add_le_add_left,
--   lt_of_add_lt_add_left := lt_of_add_lt_add_left,
--   ..MyNat.add_comm_monoid, ..MyNat.partial_order}
-- instance : canonically_ordered_monoid MyNat :=
-- { le_iff_exists_add := le_iff_exists_add,
--   bot := 0,
--   bot_le := zero_le,
--   ..MyNat.ordered_comm_monoid,
--   }
-- instance : ordered_cancel_comm_monoid MyNat :=
-- { add_left_cancel := add_left_cancel,
--   add_right_cancel := add_right_cancel,
--   le_of_add_le_add_left := le_of_add_le_add_left,
--   ..MyNat.ordered_comm_monoid}

def 
succ_lt_succ_iff: ∀ (a b : MyNat), succ a < succ b ↔ a < b
succ_lt_succ_iff (
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
  repeat
a, b: MyNat
succ a < succ b ↔ a < b rw [
a, b: MyNat
succ a < succ b ↔ a < b
lt_iff_succ_le: ∀ (a b : MyNat), a < b ↔ succ a ≤ b
lt_iff_succ_le
a, b: MyNat
succ (succ a) ≤ succ b ↔ succ a ≤ b]
a, b: MyNat
succ (succ a) ≤ succ b ↔ a < b
  exact 
succ_le_succ_iff: ∀ (m n : MyNat), succ m ≤ succ n ↔ m ≤ n
succ_le_succ_iff 
_: MyNat
_ 
_: MyNat
_
Goals accomplished! 🐙

-- multiplication

theorem 
mul_le_mul_of_nonneg_left: ∀ (a b c : MyNat), a ≤ b → 0 ≤ c → c * a ≤ c * b
mul_le_mul_of_nonneg_left (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b → 
0: MyNat
0 ≤ 
c: MyNat
c → 
c: MyNat
c * 
a: MyNat
a ≤ 
c: MyNat
c * 
b: MyNat
b := by
a, b, c: MyNat
a ≤ b → 0 ≤ c → c * a ≤ c * b
  intro 
hab: a ≤ b
hab
a, b, c: MyNat
hab: a ≤ b
0 ≤ c → c * a ≤ c * b
  intro
a, b, c: MyNat
hab: a ≤ b
0 ≤ c → c * a ≤ c * b 
h0: 0 ≤ c
h0
Warning: unused variable `h0` [linter.unusedVariables]
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ c * b
  cases 
hab: a ≤ b
hab with
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ c * b
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
d: MyNat
d 
hd: b = a + d
hd =>
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * b
    rw [
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * b
hd: b = a + d
hd
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * (a + d)]
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * (a + d)
    rw [
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * (a + d)
mul_add: ∀ (t a b : MyNat), t * (a + b) = t * a + t * b
mul_add
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * a + c * d]
a, b, c: MyNat
h0: 0 ≤ c
d: MyNat
hd: b = a + d
intro
c * a ≤ c * a + c * d
    use 
c: MyNat
c * 
d: MyNat
d
Goals accomplished! 🐙

theorem 
mul_le_mul_of_nonneg_right: ∀ (a b c : MyNat), a ≤ b → 0 ≤ c → a * c ≤ b * c
mul_le_mul_of_nonneg_right (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b → 
0: MyNat
0 ≤ 
c: MyNat
c → 
a: MyNat
a * 
c: MyNat
c ≤ 
b: MyNat
b * 
c: MyNat
c := by
a, b, c: MyNat
a ≤ b → 0 ≤ c → a * c ≤ b * c
  intro 
hab: a ≤ b
hab
a, b, c: MyNat
hab: a ≤ b
0 ≤ c → a * c ≤ b * c
  intro 
h0: 0 ≤ c
h0
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
a * c ≤ b * c
  rw [
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
a * c ≤ b * c
mul_comm: ∀ (a b : MyNat), a * b = b * a
mul_comm
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ b * c]
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ b * c
  rw [
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ b * c
mul_comm: ∀ (a b : MyNat), a * b = b * a
mul_comm 
b: MyNat
b
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ c * b]
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
c * a ≤ c * b
  apply 
mul_le_mul_of_nonneg_left: ∀ (a b c : MyNat), a ≤ b → 0 ≤ c → c * a ≤ c * b
mul_le_mul_of_nonneg_left
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
a
a ≤ b
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
a
0 ≤ c
  assumption
a, b, c: MyNat
hab: a ≤ b
h0: 0 ≤ c
a
0 ≤ c
  assumption
Goals accomplished! 🐙

theorem 
mul_lt_mul_of_pos_left: ∀ (a b c : MyNat), a < b → 0 < c → c * a < c * b
mul_lt_mul_of_pos_left (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → 
0: MyNat
0 < 
c: MyNat
c → 
c: MyNat
c * 
a: MyNat
a < 
c: MyNat
c * 
b: MyNat
b := by
a, b, c: MyNat
a < b → 0 < c → c * a < c * b
  intro 
hab: a < b
hab
a, b, c: MyNat
hab: a < b
0 < c → c * a < c * b
  intro 
hc: 0 < c
hc
a, b, c: MyNat
hab: a < b
hc: 0 < c
c * a < c * b
  cases 
c: MyNat
c with
a, b, c: MyNat
hab: a < b
hc: 0 < c
c * a < c * b
  | 
zero: MyNat
zero =>
a, b: MyNat
hab: a < b
hc: 0 < zero
zero
zero * a < zero * b
    exfalso
a, b: MyNat
hab: a < b
hc: 0 < zero
zero.h
False
    exact 
lt_irrefl: ∀ (a : MyNat), ¬a < a
lt_irrefl 
0: MyNat
0 
hc: 0 < zero
hc
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
d: MyNat
d =>
a, b: MyNat
hab: a < b
d: MyNat
hc: 0 < succ d
succ
succ d * a < succ d * b
    clear 
hc: 0 < succ d
hc
a, b: MyNat
hab: a < b
d: MyNat
succ
succ d * a < succ d * b
    induction 
d: MyNat
d with
a, b: MyNat
hab: a < b
d: MyNat
succ
succ d * a < succ d * b
    | 
zero: MyNat
zero =>
a, b: MyNat
hab: a < b
succ.zero
succ zero * a < succ zero * b
      rw [
a, b: MyNat
hab: a < b
succ.zero
succ zero * a < succ zero * b
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul,
a, b: MyNat
hab: a < b
succ.zero
zero * a + a < succ zero * b 
zero_is_0: zero = 0
zero_is_0,
a, b: MyNat
hab: a < b
succ.zero
0 * a + a < succ 0 * b 
zero_mul: ∀ (m : MyNat), 0 * m = 0
zero_mul
a, b: MyNat
hab: a < b
succ.zero
0 + a < succ 0 * b]
a, b: MyNat
hab: a < b
succ.zero
0 + a < succ 0 * b
      rw [
a, b: MyNat
hab: a < b
succ.zero
0 + a < succ 0 * b
zero_add: ∀ (n : MyNat), 0 + n = n
zero_add,
a, b: MyNat
hab: a < b
succ.zero
a < succ 0 * b 
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul,
a, b: MyNat
hab: a < b
succ.zero
a < 0 * b + b 
zero_mul: ∀ (m : MyNat), 0 * m = 0
zero_mul,
a, b: MyNat
hab: a < b
succ.zero
a < 0 + b 
zero_add: ∀ (n : MyNat), 0 + n = n
zero_add
a, b: MyNat
hab: a < b
succ.zero
a < b]
a, b: MyNat
hab: a < b
succ.zero
a < b
      exact 
hab: a < b
hab
Goals accomplished! 🐙
    | 
succ: MyNat → MyNat
succ 
e: MyNat
e 
he: succ e * a < succ e * b
he =>
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ (succ e) * a < succ (succ e) * b
      rw [
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ (succ e) * a < succ (succ e) * b
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ (succ e) * b]
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ (succ e) * b
      rw [
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ (succ e) * b
succ_mul: ∀ (a b : MyNat), succ a * b = a * b + b
succ_mul (
succ: MyNat → MyNat
succ 
e: MyNat
e)
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ e * b + b]
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ e * b + b
      have 
h: succ e * a + a < succ e * b + a
h : 
succ: MyNat → MyNat
succ 
e: MyNat
e * 
a: MyNat
a + 
a: MyNat
a < 
succ: MyNat → MyNat
succ 
e: MyNat
e * 
b: MyNat
b + 
a: MyNat
a :=
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ.succ
succ e * a + a < succ e * b + b by
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
succ e * a + a < succ e * b + a
        exact 
add_lt_add_right: ∀ (a b : MyNat), a < b → ∀ (c : MyNat), a + c < b + c
add_lt_add_right 
_: MyNat
_ 
_: MyNat
_ 
he: succ e * a < succ e * b
he 
_: MyNat
_
Goals accomplished! 🐙
      apply 
lt_trans: ∀ (a b c : MyNat), a < b → b < c → a < c
lt_trans 
_: MyNat
_ 
_: MyNat
_ 
_: MyNat
_ 
h: succ e * a + a < succ e * b + a
h
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
succ e * b + a < succ e * b + b
      rw [
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
succ e * b + a < succ e * b + b
add_comm: ∀ (a b : MyNat), a + b = b + a
add_comm
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
a + succ e * b < succ e * b + b]
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
a + succ e * b < succ e * b + b
      rw [
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
a + succ e * b < succ e * b + b
add_comm: ∀ (a b : MyNat), a + b = b + a
add_comm 
_: MyNat
_ 
b: MyNat
b
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
a + succ e * b < b + succ e * b]
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ
a + succ e * b < b + succ e * b
      apply 
add_lt_add_right: ∀ (a b : MyNat), a < b → ∀ (c : MyNat), a + c < b + c
add_lt_add_right
a, b: MyNat
hab: a < b
e: MyNat
he: succ e * a < succ e * b
h: succ e * a + a < succ e * b + a
succ.succ.a
a < b
      assumption
Goals accomplished! 🐙

theorem 
mul_lt_mul_of_pos_right: ∀ (a b c : MyNat), a < b → 0 < c → a * c < b * c
mul_lt_mul_of_pos_right (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c : 
MyNat: Type
MyNat) : 
a: MyNat
a < 
b: MyNat
b → 
0: MyNat
0 < 
c: MyNat
c → 
a: MyNat
a * 
c: MyNat
c < 
b: MyNat
b * 
c: MyNat
c := by
a, b, c: MyNat
a < b → 0 < c → a * c < b * c
  intros 
ha: a < b
ha 
h0: 0 < c
h0
a, b, c: MyNat
ha: a < b
h0: 0 < c
a * c < b * c
  rw [
a, b, c: MyNat
ha: a < b
h0: 0 < c
a * c < b * c
mul_comm: ∀ (a b : MyNat), a * b = b * a
mul_comm
a, b, c: MyNat
ha: a < b
h0: 0 < c
c * a < b * c]
a, b, c: MyNat
ha: a < b
h0: 0 < c
c * a < b * c
  rw [
a, b, c: MyNat
ha: a < b
h0: 0 < c
c * a < b * c
mul_comm: ∀ (a b : MyNat), a * b = b * a
mul_comm 
b: MyNat
b
a, b, c: MyNat
ha: a < b
h0: 0 < c
c * a < c * b]
a, b, c: MyNat
ha: a < b
h0: 0 < c
c * a < c * b
  apply 
mul_lt_mul_of_pos_left: ∀ (a b c : MyNat), a < b → 0 < c → c * a < c * b
mul_lt_mul_of_pos_left
a, b, c: MyNat
ha: a < b
h0: 0 < c
a
a < b
a, b, c: MyNat
ha: a < b
h0: 0 < c
a
0 < c
  assumption
a, b, c: MyNat
ha: a < b
h0: 0 < c
a
0 < c
  assumption
Goals accomplished! 🐙

-- BUGBUG todo
-- And now another achievement! The naturals are an ordered semiring.
-- instance : ordered_semiring MyNat :=
-- { mul_le_mul_of_nonneg_left := mul_le_mul_of_nonneg_left,
--   mul_le_mul_of_nonneg_right := mul_le_mul_of_nonneg_right,
--   mul_lt_mul_of_pos_left := mul_lt_mul_of_pos_left,
--   mul_lt_mul_of_pos_right := mul_lt_mul_of_pos_right,
--   ..MyNat.semiring,
--   ..MyNat.ordered_cancel_comm_monoid
-- }

-- The Orderd semiring would give us this theorem, but we can do it manually instead.
lemma 
mul_le_mul: ∀ {a b c d : MyNat}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
mul_le_mul {
a: MyNat
a 
b: MyNat
b 
c: MyNat
c 
d: MyNat
d : 
MyNat: Type
MyNat} (
hac: a ≤ c
hac : 
a: MyNat
a ≤ 
c: MyNat
c) (
hbd: b ≤ d
hbd : 
b: MyNat
b ≤ 
d: MyNat
d) (
nn_b: 0 ≤ b
nn_b : 
0: MyNat
0 ≤ 
b: MyNat
b) (
nn_c: 0 ≤ c
nn_c : 
0: MyNat
0 ≤ 
c: MyNat
c) : 
a: MyNat
a * 
b: MyNat
b ≤ 
c: MyNat
c * 
d: MyNat
d := by
a, b, c, d: MyNat
hac: a ≤ c
hbd: b ≤ d
nn_b: 0 ≤ b
nn_c: 0 ≤ c
a * b ≤ c * d
  calc
    
a: MyNat
a * 
b: MyNat
b ≤ 
c: MyNat
c * 
b: MyNat
b := 
mul_le_mul_of_nonneg_right: ∀ (a b c : MyNat), a ≤ b → 0 ≤ c → a * c ≤ b * c
mul_le_mul_of_nonneg_right 
_: MyNat
_ 
_: MyNat
_ 
_: MyNat
_ 
hac: a ≤ c
hac 
nn_b: 0 ≤ b
nn_b
    
_: MyNat
_ ≤ 
c: MyNat
c * 
d: MyNat
d := 
mul_le_mul_of_nonneg_left: ∀ (a b c : MyNat), a ≤ b → 0 ≤ c → c * a ≤ c * b
mul_le_mul_of_nonneg_left 
_: MyNat
_ 
_: MyNat
_ 
_: MyNat
_ 
hbd: b ≤ d
hbd 
nn_c: 0 ≤ c
nn_c
Goals accomplished! 🐙

lemma 
le_mul: ∀ (a b c d : MyNat), a ≤ b → c ≤ d → a * c ≤ b * d
le_mul (
a: MyNat
a 
b: MyNat
b 
c: MyNat
c 
d: MyNat
d : 
MyNat: Type
MyNat) : 
a: MyNat
a ≤ 
b: MyNat
b → 
c: MyNat
c ≤ 
d: MyNat
d → 
a: MyNat
a * 
c: MyNat
c ≤ 
b: MyNat
b * 
d: MyNat
d := by
a, b, c, d: MyNat
a ≤ b → c ≤ d → a * c ≤ b * d
  intros 
hab: a ≤ b
hab 
hcd: c ≤ d
hcd
a, b, c, d: MyNat
hab: a ≤ b
hcd: c ≤ d
a * c ≤ b * d
  induction 
a: MyNat
a with
a, b, c, d: MyNat
hab: a ≤ b
hcd: c ≤ d
a * c ≤ b * d
  | 
zero: MyNat
zero =>
b, c, d: MyNat
hcd: c ≤ d
hab: zero ≤ b
zero
zero * c ≤ b * d
    rw [
b, c, d: MyNat
hcd: c ≤ d
hab: zero ≤ b
zero
zero * c ≤ b * d
zero_is_0: zero = 0
zero_is_0,
b, c, d: MyNat
hcd: c ≤ d
hab: zero ≤ b
zero
0 * c ≤ b * d 
zero_mul: ∀ (m : MyNat), 0 * m = 0
zero_mul
b, c, d: MyNat
hcd: c ≤ d
hab: zero ≤ b
zero
0 ≤ b * d]
b, c, d: MyNat
hcd: c ≤ d
hab: zero ≤ b
zero
0 ≤ b * d
    apply 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
t: MyNat
t
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
succ
succ t * c ≤ b * d 
Ht: t ≤ b → t * c ≤ b * d
Ht
Warning: unused variable `Ht` [linter.unusedVariables]
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
succ
succ t * c ≤ b * d =>
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
succ
succ t * c ≤ b * d
    have 
cz: 0 ≤ c
cz : 
0: MyNat
0 ≤ 
c: MyNat
c :=
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
succ
succ t * c ≤ b * d by
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
0 ≤ c
      apply 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le
Goals accomplished! 🐙
    have 
bz: 0 ≤ b
bz : 
0: MyNat
0 ≤ 
b: MyNat
b :=
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
cz: 0 ≤ c
succ
succ t * c ≤ b * d by
b, c, d: MyNat
hcd: c ≤ d
t: MyNat
Ht: t ≤ b → t * c ≤ b * d
hab: succ t ≤ b
cz: 0 ≤ c
0 ≤ b
      apply 
zero_le: ∀ (a : MyNat), 0 ≤ a
zero_le
Goals accomplished! 🐙
    apply 
mul_le_mul: ∀ {a b c d : MyNat}, a ≤ c → b ≤ d → 0 ≤ b → 0 ≤ c → a * b ≤ c * d
mul_le_mul 
hab: succ t ≤ b
hab 
hcd: c ≤ d
hcd 
cz: 0 ≤ c
cz 
bz: 0 ≤ b
bz
Goals accomplished! 🐙

lemma 
pow_le: ∀ (m n a : MyNat), m ≤ n → m ^ a ≤ n ^ a
pow_le (
m: MyNat
m 
n: MyNat
n 
a: MyNat
a : 
MyNat: Type
MyNat) : 
m: MyNat
m ≤ 
n: MyNat
n → 
m: MyNat
m ^ 
a: MyNat
a ≤ 
n: MyNat
n ^ 
a: MyNat
a := by
m, n, a: MyNat
m ≤ n → m ^ a ≤ n ^ a
  intro 
h: m ≤ n
h
m, n, a: MyNat
h: m ≤ n
m ^ a ≤ n ^ a
  induction 
a: MyNat
a with
m, n, a: MyNat
h: m ≤ n
m ^ a ≤ n ^ a
  | 
zero: MyNat
zero =>
m, n: MyNat
h: m ≤ n
zero
m ^ zero ≤ n ^ zero
    rw [
m, n: MyNat
h: m ≤ n
zero
m ^ zero ≤ n ^ zero
zero_is_0: zero = 0
zero_is_0,
m, n: MyNat
h: m ≤ n
zero
m ^ 0 ≤ n ^ 0 
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero,
m, n: MyNat
h: m ≤ n
zero
1 ≤ n ^ 0 
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero
m, n: MyNat
h: m ≤ n
zero
1 ≤ 1]
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
t: MyNat
t 
Ht: m ^ t ≤ n ^ t
Ht =>
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ
m ^ succ t ≤ n ^ succ t
    rw [
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ
m ^ succ t ≤ n ^ succ t
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ,
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ
m ^ t * m ≤ n ^ succ t 
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ
m ^ t * m ≤ n ^ t * n]
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ
m ^ t * m ≤ n ^ t * n
    apply 
le_mul: ∀ (a b c d : MyNat), a ≤ b → c ≤ d → a * c ≤ b * d
le_mul
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ.a
m ^ t ≤ n ^ t
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ.a
m ≤ n
    assumption
m, n: MyNat
h: m ≤ n
t: MyNat
Ht: m ^ t ≤ n ^ t
succ.a
m ≤ n
    assumption
Goals accomplished! 🐙

lemma 
strong_induction_aux: ∀ (P : MyNat → Prop), (∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m) → ∀ (n c : MyNat), c < n → P c
strong_induction_aux (
P: MyNat → Prop
P : 
MyNat: Type
MyNat → 
Prop: Type
Prop)
  (
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
IH : ∀ 
m: MyNat
m : 
MyNat: Type
MyNat, (∀ 
b: MyNat
b : 
MyNat: Type
MyNat, 
b: MyNat
b < 
m: MyNat
m → 
P: MyNat → Prop
P 
b: MyNat
b) → 
P: MyNat → Prop
P 
m: MyNat
m)
  (
n: MyNat
n : 
MyNat: Type
MyNat) : ∀ 
c: MyNat
c < 
n: MyNat
n, 
P: MyNat → Prop
P 
c: MyNat
c := by
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
n: MyNat
∀ (c : MyNat), c < n → P c
  induction 
n: MyNat
n with
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
n: MyNat
∀ (c : MyNat), c < n → P c
  | 
zero: MyNat
zero =>
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
zero
∀ (c : MyNat), c < zero → P c
    intro 
c: MyNat
c
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
c: MyNat
zero
c < zero → P c
    intro 
hc: c < zero
hc
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
c: MyNat
hc: c < zero
zero
P c
    exfalso
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
c: MyNat
hc: c < zero
zero.h
False
    revert 
hc: c < zero
hc
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
c: MyNat
zero.h
c < zero → False
    exact 
not_lt_zero: ∀ (a : MyNat), ¬a < 0
not_lt_zero 
c: MyNat
c
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
d: MyNat
d 
hd: ∀ (c : MyNat), c < d → P c
hd =>
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
succ
∀ (c : MyNat), c < succ d → P c
    intros 
e: MyNat
e 
he: e < succ d
he
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e < succ d
succ
P e
    rw [
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e < succ d
succ
P e
lt_succ_iff_le: ∀ (m n : MyNat), m < succ n ↔ m ≤ n
lt_succ_iff_le
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
succ
P e]
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
succ
P e at 
he: e < succ d
he
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
succ
P e
    apply 
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
IH
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
succ.a
∀ (b : MyNat), b < e → P b
    intros 
b: MyNat
b 
hb: b < e
hb
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
b: MyNat
hb: b < e
succ.a
P b
    apply 
hd: ∀ (c : MyNat), c < d → P c
hd
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m
d: MyNat
hd: ∀ (c : MyNat), c < d → P c
e: MyNat
he: e ≤ d
b: MyNat
hb: b < e
succ.a.a
b < d
    exact 
lt_of_lt_of_le: ∀ (a b c : MyNat), a < b → b ≤ c → a < c
lt_of_lt_of_le 
_: MyNat
_ 
_: MyNat
_ 
_: MyNat
_ 
hb: b < e
hb 
he: e ≤ d
he
Goals accomplished! 🐙

theorem 
strong_induction: ∀ (P : MyNat → Prop), (∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m) → ∀ (n : MyNat), P n
strong_induction (
P: MyNat → Prop
P : 
MyNat: Type
MyNat → 
Prop: Type
Prop)
  (
IH: ∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m
IH : ∀ 
m: MyNat
m : 
MyNat: Type
MyNat, (∀ 
d: MyNat
d : 
MyNat: Type
MyNat, 
d: MyNat
d < 
m: MyNat
m → 
P: MyNat → Prop
P 
d: MyNat
d) → 
P: MyNat → Prop
P 
m: MyNat
m) :
  ∀ 
n: MyNat
n, 
P: MyNat → Prop
P 
n: MyNat
n := by
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m
∀ (n : MyNat), P n
  intro 
n: MyNat
n
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m
n: MyNat
P n
  apply 
strong_induction_aux: ∀ (P : MyNat → Prop), (∀ (m : MyNat), (∀ (b : MyNat), b < m → P b) → P m) → ∀ (n c : MyNat), c < n → P c
strong_induction_aux 
P: MyNat → Prop
P 
IH: ∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m
IH (
succ: MyNat → MyNat
succ 
n: MyNat
n)
P: MyNat → Prop
IH: ∀ (m : MyNat), (∀ (d : MyNat), d < m → P d) → P m
n: MyNat
a
n < succ n
  exact 
lt_succ_self: ∀ (n : MyNat), n < succ n
lt_succ_self 
n: MyNat
n
Goals accomplished! 🐙