no goals
F : Type ?u.184342
α : Type ?u.184345
β : Type ?u.184348
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
z : ℤ
a✝ : α
k : Type u_1
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
b✝ a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ⌊b / a⌋ • a = b
rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel b ha]