proposition: Lemma sqrt_lt_R0 : forall x:R, 0 < x -> 0 < sqrt x.
proof: Proof. intros x H1; apply Rsqr_incrst_0; [ rewrite Rsqr_0; rewrite Rsqr_sqrt; [ assumption | left; assumption ] | right; reflexivity | apply (sqrt_positivity x (Rlt_le 0 x H1)) ]. Qed.
imports: Rbase Rfunctions Rsqrt_def