From f16545cc950129ec44c45d7f8cecf9f0e7cd48d1 Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 17 Jul 2006 17:29:09 +0000
Subject: Renommage sqtr_lem_1 (bug 1189)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/R_sqrt.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3