proposition: Lemma sqrt_le_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x <= sqrt y -> x <= y.
proof: Proof. intros x y H1 H2 H3; generalize (Rsqr_incr_1 (sqrt x) (sqrt y) H3 (sqrt_positivity x H1) (sqrt_positivity y H2)); intro H4; rewrite (Rsqr_sqrt x H1) in H4; rewrite (Rsqr_sqrt y H2) in H4; assumption. Qed.
imports: Rbase Rfunctions Rsqrt_def