proposition: Lemma Rsqr_incr_0 : forall x y:R, Rsqr x <= Rsqr y -> 0 <= x -> 0 <= y -> x <= y.
proof: Proof. intros; destruct (Rle_dec x y) as [Hle|Hnle]; [ assumption | cut (y < x); [ intro; unfold Rsqr in H; generalize (Rmult_le_0_lt_compat y x y x H1 H1 H2 H2); intro; generalize (Rle_lt_trans (x * x) (y * y) (x * x) H H3); intro; elim (Rlt_irrefl (x * x) H4) | auto with real ] ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun