proposition: Lemma Ratan_seq_opp : forall x n, Ratan_seq (-x) n = -Ratan_seq x n.
proof: Proof. intros x n; unfold Ratan_seq. rewrite !pow_add, !pow_mult, !pow_1. unfold Rdiv; replace ((-x) ^ 2) with (x ^ 2) by ring; ring. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia