Library Coq.setoid_ring.ArithRing
Require
Import
Mult
.
Require
Import
BinNat
.
Require
Import
Nnat
.
Require
Export
Ring
.
Lemma
natSRth
:
semi_ring_theory
O
(
S
O
)
plus
mult
(@
eq
nat
).
Lemma
nat_morph_N
:
semi_morph
0 1
plus
mult
(
eq
(
A
:=
nat
))
0%
N
1%
N
Nplus
Nmult
Neq_bool
nat_of_N
.
Ltac
natcst
t
:=
match
isnatcst
t
with
true
=>
constr
:(
N_of_nat
t
)
|
_
=>
constr
:
InitialRing.NotConstant
end
.
Ltac
Ss_to_add
f
acc
:=
match
f
with
|
S
?
f1
=>
Ss_to_add
f1
(
S
acc
)
|
_
=>
constr
:(
acc
+
f
)%
nat
end
.
Ltac
natprering
:=
match
goal
with
|-
context
C
[
S
?
p
] =>
match
p
with
O
=>
fail
1
|
p
=>
match
isnatcst
p
with
|
true
=>
fail
1
|
false
=>
let
v
:=
Ss_to_add
p
(
S
0)
in
fold
v
;
natprering
end
end
|
_
=>
idtac
end
.
Add
Ring
natr
:
natSRth
(
morphism
nat_morph_N
,
constants
[
natcst
],
preprocess
[
natprering
]).