[GOAL]
a : ℕ
ha : a ≤ pred a
⊢ IsMin a
[PROOFSTEP]
cases a
[GOAL]
case zero
ha : zero ≤ pred zero
⊢ IsMin zero
[PROOFSTEP]
exact isMin_bot
[GOAL]
case succ
n✝ : ℕ
ha : succ n✝ ≤ pred (succ n✝)
⊢ IsMin (succ n✝)
[PROOFSTEP]
exact (not_succ_le_self _ ha).elim
[GOAL]
a b : ℕ
h : a < b
⊢ a ≤ pred b
[PROOFSTEP]
cases b
[GOAL]
case zero
a : ℕ
h : a < zero
⊢ a ≤ pred zero
[PROOFSTEP]
exact (a.not_lt_zero h).elim
[GOAL]
case succ
a n✝ : ℕ
h : a < succ n✝
⊢ a ≤ pred (succ n✝)
[PROOFSTEP]
exact le_of_succ_le_succ h
[GOAL]
a b : ℕ
h : pred a < b
⊢ a ≤ b
[PROOFSTEP]
cases a
[GOAL]
case zero
b : ℕ
h : pred zero < b
⊢ zero ≤ b
[PROOFSTEP]
exact b.zero_le
[GOAL]
case succ
b n✝ : ℕ
h : pred (succ n✝) < b
⊢ succ n✝ ≤ b
[PROOFSTEP]
exact h
[GOAL]
a n : ℕ
⊢ succ^[n + 1] a = a + (n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', add_succ]
[GOAL]
a n : ℕ
⊢ (succ ∘ succ^[n]) a = succ (a + n)
[PROOFSTEP]
exact congr_arg _ (succ_iterate a n)
[GOAL]
a n : ℕ
⊢ pred^[n + 1] a = a - (n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', sub_succ]
[GOAL]
a n : ℕ
⊢ (pred ∘ pred^[n]) a = pred (a - n)
[PROOFSTEP]
exact congr_arg _ (pred_iterate a n)
[GOAL]
a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b
[PROOFSTEP]
rw [succ_eq_succ, succ_iterate, add_tsub_cancel_of_le h]
[GOAL]
a b : ℕ
h : a ≤ b
⊢ Order.pred^[b - a] b = a
[PROOFSTEP]
rw [pred_eq_pred, pred_iterate, tsub_tsub_cancel_of_le h]
