import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import AdvancedAdditionWorld.Level1 --  succ_inj
import AdvancedAdditionWorld.Level9 --  zero_ne_succ
namespace MyNat
open MyNat

Inequality world.

Level 13: not_succ_le_self

Turns out that ¬ P is by definition P → false, so you can just start this one with intro h if you like.

Lemma : not_succ_le_self

For all naturals a, succ a is not at most a.

theorem 
not_succ_le_self: ∀ (a : MyNat), ¬succ a ≤ a
not_succ_le_self (
a: MyNat
a : 
MyNat: Type
MyNat) : ¬ (
succ: MyNat → MyNat
succ 
a: MyNat
a ≤ 
a: MyNat
a) := by
a: MyNat
¬succ a ≤ a
  intro 
h: succ a ≤ a
h
a: MyNat
h: succ a ≤ a
False
  cases 
h: succ a ≤ a
h with
a: MyNat
h: succ a ≤ a
False
  | 
_: ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
_ 
c: MyNat
c 
h: a = succ a + c
h =>
a, c: MyNat
h: a = succ a + c
intro
False
    induction 
a: MyNat
a with
a, c: MyNat
h: a = succ a + c
intro
False
    | 
zero: MyNat
zero =>
c: MyNat
h: zero = succ zero + c
intro.zero
False
      rw [
c: MyNat
h: zero = succ zero + c
intro.zero
False
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
c: MyNat
h: zero = succ (zero + c)
intro.zero
False]
c: MyNat
h: zero = succ (zero + c)
intro.zero
False at 
h: zero = succ zero + c
h
c: MyNat
h: zero = succ (zero + c)
intro.zero
False
      exact 
zero_ne_succ: ∀ (a : MyNat), 0 ≠ succ a
zero_ne_succ 
_: MyNat
_ 
h: zero = succ (zero + c)
h
Goals accomplished! 🐙
    | 
succ: MyNat → MyNat
succ 
d: MyNat
d 
hd: d = succ d + c → False
hd =>
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d) + c
intro.succ
False
      rw [
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d) + c
intro.succ
False
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d + c)
intro.succ
False]
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d + c)
intro.succ
False at 
h: succ d = succ (succ d) + c
h
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d + c)
intro.succ
False
      apply 
hd: d = succ d + c → False
hd
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d + c)
intro.succ
d = succ d + c
      apply 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj
c, d: MyNat
hd: d = succ d + c → False
h: succ d = succ (succ d + c)
intro.succ.a
succ d = succ (succ d + c)
      exact 
h: succ d = succ (succ d + c)
h
Goals accomplished! 🐙

Pro tip:

The conv tactic allows you to perform targeted rewriting on a goal or hypothesis, by focusing on particular subexpressions.

  conv =>
    lhs
    rw hc

This is an incantation which rewrites hc only on the left hand side of the goal. You didn't need to use conv in the above proof but it's a helpful trick when rw is rewriting too much.

For a deeper discussion on conv see Conversion Tactic Mode

Next up Level 14