rw [sub_add_cancel]
f : ℚ → ℝ
x : ℚ
hx : 1 ≤ x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H2 : ∀ (x y : ℚ), 0 < x → 0 < y → f x + f y ≤ f (x + y)
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hx0 : ↑x - 1 < f ↑⌊x⌋₊
h_lt : ↑⌊x⌋₊ < x
⊢ f (x - ↑⌊x⌋₊ + ↑⌊x⌋₊) = f x
no goals