proposition: Lemma exp_seq_neq : forall n : nat, exp_seq n <> 0.
proof: Proof. intro n ; unfold exp_seq ; apply Cinv_neq_0_compat ; apply not_0_INC ; apply fact_neq_0. Qed.
imports: Lia Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_usual_facts Rtactic MyRIneq Cprop_base Csequence Csequence_facts Cpser_def Cpser_base_facts Cpser_facts Cseries Cseries_facts Cdefinitions Canalysis_def