diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /theories/Numbers/Integer/Abstract | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcf..c2fa69e5 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - |