no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a
cases a <;> exact (_root_.zero_add _).symm
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
b : ZNum
⊢ ↑(b + 0) = ↑b + ↑0
cases b <;> exact (_root_.add_zero _).symm
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(pos a + neg b) = ↑(pos a) + ↑(neg b)
simpa only [sub_eq_add_neg] using PosNum.cast_sub' (α := α) _ _
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + ↑(-↑a) = ↑(-↑a + ↑b)
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑b + -↑a = -↑a + ↑b
rw [← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_neg, ← Int.cast_add (-a)]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑b + ↑(-↑a) = ↑(-↑a + ↑b)
simp [add_comm]
no goals
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ -↑(a + b) = -↑a + -↑b
rw [PosNum.cast_add, neg_eq_iff_eq_neg, neg_add_rev, neg_neg, neg_neg,
    ← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_add, ← Int.cast_add, add_comm]