proposition: Lemma sum_Ratan_seq_opp : forall x n, sum_f_R0 (tg_alt (Ratan_seq (- x))) n = - sum_f_R0 (tg_alt (Ratan_seq x)) n.
proof: Proof. intros x n; replace (-sum_f_R0 (tg_alt (Ratan_seq x)) n) with (-1 * sum_f_R0 (tg_alt (Ratan_seq x)) n) by ring. rewrite scal_sum; apply sum_eq; intros i _; unfold tg_alt. rewrite Ratan_seq_opp; ring. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia