diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-17 17:29:09 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-17 17:29:09 +0000 |
| commit | f16545cc950129ec44c45d7f8cecf9f0e7cd48d1 (patch) | |
| tree | c5808626d5db3870c8d8ee215d173aa1bfdcf7ad /theories/Reals/R_sqrt.v | |
| parent | 324d6e27061689e74c7dafd863fa3d23a8f2716a (diff) | |
Renommage sqtr_lem_1 (bug 1189)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/R_sqrt.v')
| -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 47fc4b016..b9873d947 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 |