proposition: Lemma Datan_sum_eq :forall x n, sum_f_R0 (tg_alt (Datan_seq x)) n = (1 - (- x ^ 2) ^ S n)/(1 + x ^ 2).
proof: Proof. intros x n. assert (dif : - x ^ 2 <> 1). { nra. } replace (1 + x ^ 2) with (1 - - (x ^ 2)) by ring; rewrite <- (tech3 _ n dif). apply sum_eq; unfold tg_alt, Datan_seq; intros i _. rewrite pow_mult, <- Rpow_mult_distr. f_equal. ring. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia