proposition: Lemma ub_opp : forall x, x < PI/2 -> -PI/2 < -x.
proof: Proof. intros x h; rewrite Rdiv_opp_l; apply Ropp_lt_contravar; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia