proposition: Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x.
proof: Proof. intros. unfold sqrt. case (Rcase_abs x) as [Hlt|Hge]. - elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ Hlt H)). - rewrite Rsqrt_Rsqrt; reflexivity. Qed.
imports: Rbase Rfunctions Rsqrt_def