α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b = ⌊(b - a) / p⌋
refine' toIcoDiv_eq_of_sub_zsmul_mem_Ico hp _
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - ⌊(b - a) / p⌋ • p ∈ Set.Ico a (a + p)
rw [Set.mem_Ico, zsmul_eq_mul, ← sub_nonneg, add_comm, sub_right_comm, ← sub_lt_iff_lt_add,
  sub_right_comm _ _ a]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ 0 ≤ b - a - ↑⌊(b - a) / p⌋ * p ∧ b - a - ↑⌊(b - a) / p⌋ * p < p
exact ⟨Int.sub_floor_div_mul_nonneg _ hp, Int.sub_floor_div_mul_lt _ hp⟩