∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
  [ExistsAddOfLE R] [inst_5 : Sub R] [OrderedSub R] {x : R},
  x ≤ 1 → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n