calc (x - 1 : ℝ) < f ⌊x⌋₊ := hx0
  _ < f (x - ⌊x⌋₊) + f ⌊x⌋₊ := lt_add_of_pos_left _ (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
  _ ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   := H2 _ _ (sub_pos.mpr h_lt) (Nat.cast_pos.2 (Nat.floor_pos.2 hx))
  _ = f x                   := by rw [sub_add_cancel]
case inr
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
⊢ ↑x - 1 < f x
no goals