proposition: Lemma An_deriv_arctan_seq_explicit : (An_deriv arctan_seq == Rseq_zip (Rseq_alt sum_pow_seq) 0)%Rseq.
proof: Proof. intro n ; unfold An_deriv, arctan_seq, Rseq_zip, Rseq_shift, Rseq_mult. case (n_modulo_2 n) ; intros [p Hp] ; case (n_modulo_2 (S n)) ; intros [q Hq]. apply False_ind ; lia. assert (Hpq : (p = q)%nat) by lia ; rewrite Hq, Hpq. fold (((fun q => INR (S (2 * q))) * Rseq_alt arct_seq)%Rseq q) ; rewrite <- Rseq_alt_mult_r. apply Rmult_eq_compat_l, Rinv_r, not_0_INR ; lia. unfold zero_seq, Rseq_constant ; ring. apply False_ind ; lia. 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 Rpser_sums_facts