proposition: Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y.
proof: Proof. intros; apply Rsqr_inj; [ apply (sqrt_positivity x H) | assumption | unfold Rsqr; rewrite H1; apply (sqrt_sqrt x H) ]. Qed.
imports: Rbase Rfunctions Rsqrt_def