α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b = a + p - Int.fract ((a + p - b) / p) * p
rw [toIocMod, toIocDiv_eq_neg_floor, Int.fract]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b + ↑⌊(a + p - b) / p⌋ * p = a + p - (a + p - b - p * ↑⌊(a + p - b) / p⌋)
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - ((a + p - b) / p - ↑⌊(a + p - b) / p⌋) * p
field_simp [hp.ne.symm]
no goals
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b + ↑⌊(a + p - b) / p⌋ * p = a + p - (a + p - b - p * ↑⌊(a + p - b) / p⌋)
ring