proposition: Lemma sqrt_lt_1_alt : forall x y : R, 0 <= x < y -> sqrt x < sqrt y.
proof: Proof. intros x y (Hx, Hxy). apply Rsqr_incrst_0 ; try apply sqrt_pos. rewrite 2!Rsqr_sqrt. - exact Hxy. - apply Rlt_le. now apply Rle_lt_trans with x. - exact Hx. Qed.
imports: Rbase Rfunctions Rsqrt_def