proposition: Lemma sqr_pos : forall x, 0 <= x ^ 2.
proof: Proof. intros ; rewrite <- Rsqr_pow2 ; apply Rle_0_sqr. 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