proposition: Lemma acos_opp : forall x, acos (- x) = PI - acos x.
proof: Proof. intros x. unfold acos; repeat case Rle_dec; try lra. intros Hx1 Hx2 Hx3 Hx4. rewrite <- Rsqr_neg, Rdiv_opp_l, atan_opp. lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia