[GOAL]
n : ℕ
⊢ pred n = Option.getD (ppred n) 0
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ pred zero = Option.getD (ppred zero) 0
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ pred (succ n✝) = Option.getD (ppred (succ n✝)) 0
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
⊢ Option.getD (ppred (m - n)) 0 = Option.getD (psub m (n + 1)) 0
[PROOFSTEP]
rw [sub_eq_psub m n, psub]
[GOAL]
m n : ℕ
⊢ Option.getD (ppred (Option.getD (psub m n) 0)) 0 = Option.getD (psub m n >>= ppred) 0
[PROOFSTEP]
cases psub m n
[GOAL]
case none
m n : ℕ
⊢ Option.getD (ppred (Option.getD none 0)) 0 = Option.getD (none >>= ppred) 0
[PROOFSTEP]
rfl
[GOAL]
case some
m n val✝ : ℕ
⊢ Option.getD (ppred (Option.getD (some val✝) 0)) 0 = Option.getD (some val✝ >>= ppred) 0
[PROOFSTEP]
rfl
[GOAL]
m : ℕ
⊢ ppred 0 = some m ↔ succ m = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
m : ℕ
⊢ ppred 0 = some m → succ m = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
m : ℕ
⊢ succ m = 0 → ppred 0 = some m
[PROOFSTEP]
intro h
[GOAL]
case mp
m : ℕ
h : ppred 0 = some m
⊢ succ m = 0
[PROOFSTEP]
contradiction
[GOAL]
case mpr
m : ℕ
h : succ m = 0
⊢ ppred 0 = some m
[PROOFSTEP]
contradiction
[GOAL]
m n : ℕ
⊢ ppred (n + 1) = some m ↔ succ m = n + 1
[PROOFSTEP]
constructor
[GOAL]
case mp
m n : ℕ
⊢ ppred (n + 1) = some m → succ m = n + 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
m n : ℕ
⊢ succ m = n + 1 → ppred (n + 1) = some m
[PROOFSTEP]
intro h
[GOAL]
case mp
m n : ℕ
h : ppred (n + 1) = some m
⊢ succ m = n + 1
[PROOFSTEP]
injection h
[GOAL]
case mpr
m n : ℕ
h : succ m = n + 1
⊢ ppred (n + 1) = some m
[PROOFSTEP]
injection h
[GOAL]
case mp
m n : ℕ
val_eq✝ : Nat.add n 0 = m
⊢ succ m = n + 1
[PROOFSTEP]
subst m
[GOAL]
case mpr
m n : ℕ
n_eq✝ : m = Nat.add n 0
⊢ ppred (n + 1) = some m
[PROOFSTEP]
subst m
[GOAL]
case mp
n : ℕ
⊢ succ (Nat.add n 0) = n + 1
[PROOFSTEP]
rfl
[GOAL]
case mpr
n : ℕ
⊢ ppred (n + 1) = some (Nat.add n 0)
[PROOFSTEP]
rfl
[GOAL]
⊢ ppred 0 = none ↔ 0 = 0
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ ppred (n + 1) = none ↔ n + 1 = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
⊢ ppred (n + 1) = none → n + 1 = 0
[PROOFSTEP]
intro
[GOAL]
case mpr
n : ℕ
⊢ n + 1 = 0 → ppred (n + 1) = none
[PROOFSTEP]
intro
[GOAL]
case mp
n : ℕ
a✝ : ppred (n + 1) = none
⊢ n + 1 = 0
[PROOFSTEP]
contradiction
[GOAL]
case mpr
n : ℕ
a✝ : n + 1 = 0
⊢ ppred (n + 1) = none
[PROOFSTEP]
contradiction
[GOAL]
m k : ℕ
⊢ psub m 0 = some k ↔ k + 0 = m
[PROOFSTEP]
simp [eq_comm]
[GOAL]
m n k : ℕ
⊢ psub m (n + 1) = some k ↔ k + (n + 1) = m
[PROOFSTEP]
apply Option.bind_eq_some.trans
[GOAL]
m n k : ℕ
⊢ (∃ a, psub m (Nat.add n 0) = some a ∧ ppred a = some k) ↔ k + (n + 1) = m
[PROOFSTEP]
simp only [psub_eq_some, ppred_eq_some]
[GOAL]
m n k : ℕ
⊢ (∃ a, a + Nat.add n 0 = m ∧ succ k = a) ↔ k + (n + 1) = m
[PROOFSTEP]
simp [add_comm, add_left_comm, Nat.succ_eq_add_one]
[GOAL]
m n : ℕ
⊢ psub m n = none ↔ m < n
[PROOFSTEP]
cases s : psub m n
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ none = none ↔ m < n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ some val✝ = none ↔ m < n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ m < n
[PROOFSTEP]
show m < n
[GOAL]
case none
m n : ℕ
s : psub m n = none
⊢ m < n
[PROOFSTEP]
refine' lt_of_not_ge fun h => _
[GOAL]
case none
m n : ℕ
s : psub m n = none
h : m ≥ n
⊢ False
[PROOFSTEP]
cases' le.dest h with k e
[GOAL]
case none.intro
m n : ℕ
s : psub m n = none
h : m ≥ n
k : ℕ
e : n + k = m
⊢ False
[PROOFSTEP]
injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
[PROOFSTEP]
show n ≤ m
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ m
[PROOFSTEP]
rw [← psub_eq_some.1 s]
[GOAL]
case some
m n val✝ : ℕ
s : psub m n = some val✝
⊢ n ≤ val✝ + n
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
m n k : ℕ
⊢ psub m (n + k) = do
    let __do_lift ← psub m n
    psub __do_lift k
[PROOFSTEP]
induction k
[GOAL]
case zero
m n : ℕ
⊢ psub m (n + zero) = do
    let __do_lift ← psub m n
    psub __do_lift zero
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
[PROOFSTEP]
simp [Option.bind_eq_bind, Option.bind_some]
[GOAL]
case succ
m n n✝ : ℕ
n_ih✝ :
  psub m (n + n✝) = do
    let __do_lift ← psub m n
    psub __do_lift n✝
⊢ psub m (n + succ n✝) = do
    let __do_lift ← psub m n
    psub __do_lift (succ n✝)
[PROOFSTEP]
simp [*, Nat.add_succ]
[GOAL]
m n : ℕ
⊢ psub' m n = psub m n
[PROOFSTEP]
rw [psub']
[GOAL]
m n : ℕ
⊢ (if n ≤ m then some (m - n) else none) = psub m n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = psub m n
case neg m n : ℕ h : ¬n ≤ m ⊢ none = psub m n
[PROOFSTEP]
exact (psub_eq_sub h).symm
[GOAL]
case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = psub m n
[PROOFSTEP]
exact (psub_eq_none.2 (not_le.1 h)).symm
