proposition: Lemma partial_sum_pow_explicit : forall x n, (1 - x) * Rseq_pps sum_pow_seq x n = 1 - x ^ S n.
proof: Proof. intros x n ; induction n. unfold Rseq_pps, sum_pow_seq, Rseq_constant ; simpl ; rewrite gt_pser_0 ; ring. unfold Rseq_pps in * ; rewrite Rseq_sum_simpl, <- tech_pow_Rmult, Rmult_plus_distr_l, IHn ; unfold gt_pser, sum_pow_seq, Rseq_constant, Rseq_mult. ring. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity