proposition: Lemma sqrt_inj : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = sqrt y -> x = y.
proof: Proof. intros; cut (Rsqr (sqrt x) = Rsqr (sqrt y)). - intro; rewrite (Rsqr_sqrt x H) in H2; rewrite (Rsqr_sqrt y H0) in H2; assumption. - rewrite H1; reflexivity. Qed.
imports: Rbase Rfunctions Rsqrt_def