[GOAL]
a : ℤ
n : ℕ
⊢ succ^[n + 1] a = a + ↑(n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', Int.ofNat_succ, ← add_assoc]
[GOAL]
a : ℤ
n : ℕ
⊢ (succ ∘ succ^[n]) a = a + ↑n + 1
[PROOFSTEP]
exact congr_arg _ (succ_iterate a n)
[GOAL]
a : ℤ
n : ℕ
⊢ pred^[n + 1] a = a - ↑(n + 1)
[PROOFSTEP]
rw [Function.iterate_succ', Int.ofNat_succ, ← sub_sub]
[GOAL]
a : ℤ
n : ℕ
⊢ (pred ∘ pred^[n]) a = a - ↑n - 1
[PROOFSTEP]
exact congr_arg _ (pred_iterate a n)
[GOAL]
a b : ℤ
h : a ≤ b
⊢ Order.succ^[toNat (b - a)] a = b
[PROOFSTEP]
rw [succ_eq_succ, succ_iterate, toNat_sub_of_le h, ← add_sub_assoc, add_sub_cancel']
[GOAL]
a b : ℤ
h : a ≤ b
⊢ Order.pred^[toNat (b - a)] b = a
[PROOFSTEP]
rw [pred_eq_pred, pred_iterate, toNat_sub_of_le h, sub_sub_cancel]
[GOAL]
z : ℤ
⊢ z - 1 ⋖ z
[PROOFSTEP]
rw [Int.covby_iff_succ_eq, sub_add_cancel]
[GOAL]
a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b
[PROOFSTEP]
rw [Nat.covby_iff_succ_eq, Int.covby_iff_succ_eq]
[GOAL]
a b : ℕ
⊢ ↑a + 1 = ↑b ↔ a + 1 = b
[PROOFSTEP]
exact Int.coe_nat_inj'
