proposition: Lemma geometric_sum (R : numFieldType) n (r : R) (Hr : r != 1) : \sum_(i < n) r ^+ i = (1 - r ^+ n) / (1 - r).
proof: Proof. elim: n => [|n Hn]; first by rewrite big_ord0 expr0 subrr mul0r. have den_neq0 : 1 - r != 0 by rewrite subr_eq0 eq_sym. rewrite big_ord_recr /= Hn; apply: canRL (mulfK den_neq0) _. by rewrite [LHS]mulrDl divfK // mulrBr mulr1 addrA subrK exprSr. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) extra_mathcomp posnum hanson_elem_arith