proposition: Lemma ps_atan_exists_1_opp : forall x h h', proj1_sig (ps_atan_exists_1 (-x) h) = -(proj1_sig (ps_atan_exists_1 x h')).
proof: Proof. intros x h h'; destruct (ps_atan_exists_1 (-x) h) as [v Pv]. destruct (ps_atan_exists_1 x h') as [u Pu]; simpl. assert (Pu' : Un_cv (fun N => (-1) * sum_f_R0 (tg_alt (Ratan_seq x)) N) (-1 * u)). { apply CV_mult;[ | assumption]. intros eps ep; exists 0%nat; intros; rewrite Rdist_eq; assumption. } assert (Pv' : Un_cv (fun N : nat => -1 * sum_f_R0 (tg_alt (Ratan_seq x)) N) v). { apply Un_cv_ext with (2 := Pv); intros n; rewrite sum_Ratan_seq_opp; ring. } replace (-u) with (-1 * u) by ring. apply UL_sequence with (1:=Pv') (2:= Pu'). Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia