English
Let R be a commutative semiring with a compatible order such that x ≤ y. Then the sum ∑_{i=0}^{n-1} x^i y^{n-1-i} multiplied by (y − x) equals y^n − x^n.
Русский
Пусть R — коммутативное полукольцо с упорядочиванием, и пусть x ≤ y. Тогда сумма ∑_{i=0}^{n-1} x^i y^{n-1-i} умноженная на (y − x) равна y^n − x^n.
LaTeX
$$$\\displaystyle \\left(\\sum_{i=0}^{n-1} x^i y^{n-1-i}\\right) (y - x) = y^n - x^n$$$
Lean4
theorem geom_sum₂_mul_of_le (hxy : x ≤ y) (n : ℕ) :
(∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (y - x) = y ^ n - x ^ n :=
by
rw [← Finset.sum_range_reflect]
convert geom_sum₂_mul_of_ge hxy n using 3
simp_all only [Finset.mem_range]
rw [mul_comm]
congr
cutsat
