diff options
author | 2000-03-10 17:46:01 +0000 | |
---|---|---|
committer | 2000-03-10 17:46:01 +0000 | |
commit | 9f8ccadf2f68ff44ee81d782b6881b9cc3c04c4b (patch) | |
tree | cb38ff6db4ade84d47f9788ae7bc821767abf638 /theories/Arith/Euclid_def.v | |
parent | 20b4a46e9956537a0bb21c5eacf2539dee95cb67 (diff) |
mise sous CVS du repertoire theories/Arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith/Euclid_def.v')
-rwxr-xr-x | theories/Arith/Euclid_def.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v new file mode 100755 index 000000000..292816f45 --- /dev/null +++ b/theories/Arith/Euclid_def.v @@ -0,0 +1,7 @@ + +(* $Id$ *) + +Require Export Mult. + +Inductive diveucl [a,b:nat] : Set + := divex : (q,r:nat)(gt b r)->(a=(plus (mult q b) r))->(diveucl a b). |