proposition: Lemma sqrt_le_1_alt : forall x y : R, x <= y -> sqrt x <= sqrt y.
proof: Proof. intros x y [Hxy|Hxy]. - destruct (Rle_or_lt 0 x) as [Hx|Hx]. + apply Rlt_le. apply sqrt_lt_1_alt. now split. + unfold sqrt at 1. destruct (Rcase_abs x) as [Hx'|Hx']. * apply sqrt_pos. * now elim Rge_not_lt with (1 := Hx'). - rewrite Hxy. apply Rle_refl. Qed.
imports: Rbase Rfunctions Rsqrt_def