no goals
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + ↑n) = ↑↑m + ↑↑n
simp [← Int.ofNat_add, Nat.cast_add]
no goals
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(↑m + -[n+1]) = ↑↑m + ↑-[n+1]
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_add_neg]
no goals
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(-[m+1] + ↑n) = ↑-[m+1] + ↑↑n
erw [cast_subNatNat, cast_ofNat, cast_negSucc, sub_eq_iff_eq_add, add_assoc,
  eq_neg_add_iff_add_eq, ← Nat.cast_add, ← Nat.cast_add, Nat.add_comm]
no goals
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[m + n + 1+1] = ↑-[m+1] + ↑-[n+1]
rw [cast_negSucc, cast_negSucc, cast_negSucc, ← neg_add_rev, ← Nat.cast_add,
  Nat.add_right_comm m n 1, Nat.add_assoc, Nat.add_comm]