proposition: Lemma GP_finite : forall (x:R) (n:nat), sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1.
proof: Proof. intros; induction n as [| n Hrecn]; simpl. - ring. - rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n). + intro H; rewrite H; simpl; ring. + apply Nat.add_1_r. Qed.
imports: ArithRing Rdefinitions Raxioms RIneq Rpow_def R_Ifp Rbasic_fun R_sqr SplitAbsolu SplitRmult ArithProp Zpower Ztac