no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIcoMod hp a b = toIcoMod hp 0 (b - a) + a
rw [toIcoMod_sub_eq_sub, zero_add, sub_add_cancel]