rw [Nat.cast_natAbs, abs_of_nonneg num_pos.le]
f : ℚ → ℝ
q : ℚ
hq : 0 < q
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hfqn : f ↑q.num ≤ f q * f ↑q.den
num_pos : 0 < q.num
hqna : ↑q.num.natAbs = q.num
⊢ f ↑q.num.natAbs = f ↑q.num
no goals