calc 1 ≤ x^i             := one_le_pow_of_one_le hx.le i
     _ = x^i * 1         := (mul_one _).symm
     _ ≤ x^i * y^(n-1-i) := by gcongr; apply one_le_pow_of_one_le hy.le
x y : ℝ
hx : 1 < x
hy : 1 < y
h : ∀ (n : ℕ), 0 < n → x ^ n - 1 < y ^ n
hxy : y < x
hxmy : 0 < x - y
n i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ x ^ i * y ^ (n - 1 - i)
no goals