simp [show Nat.succ 0 = 1 by rfl, pow_one]
case succ.zero
f : ℚ → ℝ
x : ℚ
hx : 1 < x
H1 : ∀ (x y : ℚ), 0 < x → 0 < y → f (x * y) ≤ f x * f y
H4 : ∀ (n : ℕ), 0 < n → ↑n ≤ f ↑n
hpn : 0 < 0 → f (x ^ 0) ≤ f x ^ 0
hn : 0 < 0 + 1
⊢ f (x ^ (0 + 1)) ≤ f x ^ (0 + 1)
no goals