diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NTimesOrder.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimesOrder.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index dc1b977aa..e644304dc 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -2,7 +2,7 @@ Require Export NOrder. Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. -Open Local Scope NatIntScope. +Open Local Scope NatScope. Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. Proof NZplus_lt_mono_l. |