proposition: Lemma sqrt_less_alt : forall x : R, 1 < x -> sqrt x < x.
proof: Proof. intros x Hx. assert (Hx1 := Rle_lt_trans _ _ _ Rle_0_1 Hx). assert (Hx2 := Rlt_le _ _ Hx1). apply Rsqr_incrst_0 ; trivial. - rewrite Rsqr_sqrt ; trivial. rewrite <- (Rmult_1_l x) at 1. now apply Rmult_lt_compat_r. - apply sqrt_pos. Qed.
imports: Rbase Rfunctions Rsqrt_def