diff options
Diffstat (limited to 'theories/Reals/R_sqrt.v')
| -rw-r--r-- | theories/Reals/R_sqrt.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 19e111f23..92f2acd4f 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -94,6 +94,10 @@ Proof. intros; unfold Rsqr; apply sqrt_square; assumption. Qed. +Lemma sqrt_pow2 : forall x, 0 <= x -> sqrt (x ^ 2) = x. +intros; simpl; rewrite Rmult_1_r, sqrt_square; auto. +Qed. + Lemma sqrt_Rsqr_abs : forall x:R, sqrt (Rsqr x) = Rabs x. Proof. intro x; rewrite Rsqr_abs; apply sqrt_Rsqr; apply Rabs_pos. @@ -517,3 +521,4 @@ Proof. reflexivity. reflexivity. Qed. + |