proposition: Lemma sqrt_eq_0 : forall x:R, 0 <= x -> sqrt x = 0 -> x = 0.
proof: Proof. intros; cut (Rsqr (sqrt x) = 0). - intro; unfold Rsqr in H1; rewrite sqrt_sqrt in H1; assumption. - rewrite H0; apply Rsqr_0. Qed.
imports: Rbase Rfunctions Rsqrt_def