no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c✝ : α
n : ℤ
a b c : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]