proposition: Lemma Rsqr_le_abs_1 : forall x y:R, Rabs x <= Rabs y -> Rsqr x <= Rsqr y.
proof: Proof. intros; rewrite (Rsqr_abs x); rewrite (Rsqr_abs y); apply (Rsqr_incr_1 (Rabs x) (Rabs y) H (Rabs_pos x) (Rabs_pos y)). Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun