K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * Int.fract a = b * a + c
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ (↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a
field_simp [fract_a_ne_zero]
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * Int.fract a = b * a + c
rw [Int.fract]
no goals
K : Type u_1
inst✝¹ : LinearOrderedField K
v : K
n : ℕ
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c
ring