proposition: Lemma plus_Rsqr_gt_0 : forall x, 1 + x ^ 2 > 0.
proof: Proof. intro m. replace 0 with (0+0) by intuition. apply Rplus_gt_ge_compat. { intuition. } destruct (total_order_T m 0) as [[m_cond|H']|?]. - replace 0 with (0*0) by intuition. replace (m ^ 2) with ((-m)^2). { apply Rle_ge ; apply Rmult_le_compat ; intuition ; apply Rlt_le ; rewrite Rmult_1_r ; intuition. } field. - rewrite H' ; right ; field. - left. intuition. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia