proposition: Lemma sqrt_square : forall x:R, 0 <= x -> sqrt (x * x) = x.
proof: Proof. intros; apply (Rsqr_inj (sqrt (Rsqr x)) x (sqrt_positivity (Rsqr x) (Rle_0_sqr x)) H); unfold Rsqr; apply (sqrt_sqrt (Rsqr x) (Rle_0_sqr x)). Qed.
imports: Rbase Rfunctions Rsqrt_def