diff options
| -rw-r--r-- | theories/Reals/R_sqrt.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 47fc4b0160..b9873d9478 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -57,7 +57,7 @@ Lemma sqrt_lem_0 : forall x y:R, 0 <= x -> 0 <= y -> sqrt x = y -> y * y = x. intros; rewrite <- H1; apply (sqrt_sqrt x H). Qed. -Lemma sqtr_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y. +Lemma sqrt_lem_1 : forall x y:R, 0 <= x -> 0 <= y -> y * y = x -> sqrt x = y. intros; apply Rsqr_inj; [ apply (sqrt_positivity x H) | assumption |