proposition: Lemma constant_is_cst : forall (c : R) (rc: infinite_cv_radius (constant_seq c)), forall x, sum _ rc x = c.
proof: Proof. intros c rc ; solve_diff_equa ; reflexivity. Qed.
imports: Rsequence_def Rsequence_base_facts Reals Rfunction_def Rfunction_facts Rextensionality Nth_derivative_def Nth_derivative_facts Rpser Rfunction_classes Dequa_def Dequa_facts Dequa_quote List