diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NPlusLt.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NPlusLt.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v index ac322a8f2b..77bd800122 100644 --- a/theories/Numbers/Natural/Axioms/NPlusLt.v +++ b/theories/Numbers/Natural/Axioms/NPlusLt.v @@ -1,12 +1,12 @@ Require Export NPlus. Require Export NLt. -Module PlusLtProperties (Export PlusModule : PlusSignature) - (Export LtModule : LtSignature with +Module PlusLtProperties (Import PlusModule : PlusSignature) + (Import LtModule : LtSignature with Module NatModule := PlusModule.NatModule). - Module Export PlusPropertiesModule := PlusProperties PlusModule. Module Export LtPropertiesModule := LtProperties LtModule. +Open Local Scope NScope. (* Print All locks up here !!! *) Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. |