proposition: Lemma One_plus_sqr_pos_lt : forall x, 0 < 1 + x ^ 2.
proof: Proof. intro x ; replace 0 with (0 + 0) by ring ; apply Rplus_lt_le_compat ; [lra | apply sqr_pos]. 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