aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Arith/Euclid.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-17 11:30:23 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-17 11:30:23 +0000
commitcc1be0bf512b421336e81099aa6906ca47e4257a (patch)
treec25fa8ed965729d7a85efa3b3292fdf7f442963d /theories/Arith/Euclid.v
parentebf9aa9f97ef0d49ed1b799c9213f78efad4fec7 (diff)
Uniformisation (Qed/Save et Implicits Arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Euclid.v')
-rw-r--r--theories/Arith/Euclid.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index c6db2917b..5a2dd1a84 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -28,7 +28,7 @@ Elim plus_assoc_l.
Elim e; Auto with arith.
Intros gtbn.
Apply divex with O n; Simpl; Auto with arith.
-Save.
+Qed.
Lemma quotient : (b:nat)(gt b O)->
(a:nat){q:nat|(EX r:nat | (a=(plus (mult q b) r))/\(gt b r))}.
@@ -43,7 +43,7 @@ Elim plus_assoc_l.
Elim H1; Auto with arith.
Intros gtbn.
Exists O; Exists n; Simpl; Auto with arith.
-Save.
+Qed.
Lemma modulo : (b:nat)(gt b O)->
(a:nat){r:nat|(EX q:nat | (a=(plus (mult q b) r))/\(gt b r))}.
@@ -58,4 +58,4 @@ Elim plus_assoc_l.
Elim H1; Auto with arith.
Intros gtbn.
Exists n; Exists O; Simpl; Auto with arith.
-Save.
+Qed.