α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
m : ℤ
⊢ toIocMod hp a (b + m • p) = toIocMod hp a b
rw [toIocMod, toIocDiv_add_zsmul, toIocMod, add_smul]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
m : ℤ
⊢ b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
abel