English
In the Archimedean setting with p > 0, the IocDiv value equals the negative floor of a certain linear expression, namely −⌊(a + p − b)/p⌋.
Русский
При Архимедовом условии и p > 0 IocDiv равен минус полная часть от (a + p − b)/p.
LaTeX
$$$$ \operatorname{toIocDiv}(hp, a, b) = -\Big\lfloor \frac{a + p - b}{p} \Big\rfloor $$$$
Lean4
theorem toIocDiv_eq_neg_floor (a b : α) : toIocDiv hp a b = -⌊(a + p - b) / p⌋ :=
by
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_
rw [Set.mem_Ioc, zsmul_eq_mul, Int.cast_neg, neg_mul, sub_neg_eq_add, ← sub_nonneg, sub_add_eq_sub_sub]
refine ⟨?_, Int.sub_floor_div_mul_nonneg _ hp⟩
rw [← add_lt_add_iff_right p, add_assoc, add_comm b, ← sub_lt_iff_lt_add, add_comm (_ * _), ← sub_lt_iff_lt_add]
exact Int.sub_floor_div_mul_lt _ hp
