proposition: Lemma Rsqr_incrst_0 : forall x y:R, Rsqr x < Rsqr y -> 0 <= x -> 0 <= y -> x < y.
proof: Proof. intros; case (Rtotal_order x y); intro; [ assumption | elim H2; intro; [ rewrite H3 in H; elim (Rlt_irrefl (Rsqr y) H) | generalize (Rmult_le_0_lt_compat y x y x H1 H1 H3 H3); intro; unfold Rsqr in H; generalize (Rlt_trans (x * x) (y * y) (x * x) H H4); intro; elim (Rlt_irrefl (x * x) H5) ] ]. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun