no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b✝ c : α
n : ℤ
a b : α
⊢ toIocDiv hp a (b - p) = toIocDiv hp a b - 1
simpa only [one_zsmul] using toIocDiv_sub_zsmul hp a b 1