Library Coq.ring.LegacyNArithRing
Require
Import
Bool
.
Require
Export
LegacyRing
.
Require
Export
ZArith_base
.
Require
Import
NArith
.
Require
Import
Eqdep_dec
.
Lemma
Neq_prop
:
forall
n
m
:
N
,
Is_true
(
Neq
n
m
) ->
n
=
m
.
Definition
NTheory
:
Semi_Ring_Theory
Nplus
Nmult
1%
N
0%
N
Neq
.
Qed
.
Add
Legacy
Semi
Ring
N
Nplus
Nmult
1%
N
0%
N
Neq
NTheory
[
Npos
0%
N
xO
xI
1%
positive
].