proposition: Lemma pow2_ge_0 : forall x, 0 <= x^2.
proof: Proof. intros x; destruct (Rle_lt_dec 0 x). - replace (x ^ 2) with (x * x) by field. apply Rmult_le_pos; assumption. - replace (x ^ 2) with ((-x) * (-x)) by field. apply Rmult_le_pos; lra. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia