proposition: Lemma Cim_Cpow_2 : forall (a : R) (n : nat), Cim ((0 +i a) ^ (2 * n)) = R0.
proof: Proof. intros a n ; induction n. simpl ; ring. replace (2 * S n)%nat with (S (S (2 * n))) by intuition. do 2 rewrite Cpow_S, Cim_mul ; rewrite IHn. rewrite Cre_mul. replace (Cre (0 +i a)) with R0 by reflexivity. repeat rewrite IHn ; ring. 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