proposition: Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.
proof: Proof. unfold Rsqr; intros r. destruct (Rlt_le_dec r 0) as [Hneg%Ropp_lt_contravar%Rlt_le | Hge0]. - rewrite Ropp_0 in Hneg; rewrite <-Rmult_opp_opp, <-(Rmult_0_l 0). now apply Rmult_le_compat; try apply Rle_refl. - now rewrite <-(Rmult_0_l 0); apply Rmult_le_compat; try apply Rle_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField