Library Coq.setoid_ring.NArithRing
Require
Export
Ring
.
Require
Import
BinPos
BinNat
.
Import
InitialRing
.
Ltac
Ncst
t
:=
match
isNcst
t
with
true
=>
t
|
_
=>
constr
:
NotConstant
end
.
Add
Ring
Nr
:
Nth
(
decidable
Neq_bool_ok
,
constants
[
Ncst
]).