proposition: Lemma tech_opp_tan : forall x y, -tan x < y -> tan (-x) < y.
proof: Proof. intros; rewrite tan_neg; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia