proposition: Lemma sqr_lt_switch : forall x y, x < y -> y <= 0 -> y² < x².
proof: Proof. intros x y xlty yneg ; rewrite (Rsqr_neg x), (Rsqr_neg y) ; apply Rsqr_incrst_1 ; lra. Qed.
imports: Rbase Rtactic Lra Ranalysis Ranalysis5 Rtrigo AltSeries Rfunctions Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Rextensionality Rpser_usual Rsequence_cv_facts MyRIneq Tactics