proposition: Theorem Rle_square : forall x y : R, (0 <= x)%R -> (0 <= y)%R -> (x * x <= y * y)%R -> (x <= y)%R.
proof: Proof. intros x y H H0 H1; case (Rle_or_lt x y); auto. intros H2; Contradict H1; apply Rlt_not_le. apply Rle_lt_trans with (x * y)%R; auto with real. apply Rmult_lt_compat_l; auto with arith. apply Rle_lt_trans with (1 := H0); auto. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)