proposition: Lemma Rsqr_le_abs_0 : forall x y:R, Rsqr x <= Rsqr y -> Rabs x <= Rabs y.
proof: Proof. intros; apply Rsqr_incr_0; repeat rewrite <- Rsqr_abs; [ assumption | apply Rabs_pos | apply Rabs_pos ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun