diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NSub.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 62d1c731c..e027c0be2 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -12,7 +12,7 @@ Require Export NMulOrder. -Module NSubPropFunct (Import N : NAxiomsSig). +Module Type NSubPropFunct (Import N : NAxiomsSig). Include NMulOrderPropFunct N. Local Open Scope NumScope. @@ -220,7 +220,7 @@ Qed. Theorem add_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). -Proof le_alt_dichotomy. +Proof. exact le_alt_dichotomy. Qed. End NSubPropFunct. |