gcongr
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
⊢ x ^ i * 1 ≤ x ^ i * y ^ (n - 1 - i)
case h
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 ≤ y ^ (n - 1 - i)