# Library Coq.ring.LegacyArithRing

Require Import Bool.
Require Export LegacyRing.
Require Export Arith.
Require Import Eqdep_dec.
Open Local Scope nat_scope.
Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m.
Hint Resolve nateq_prop: arithring.
Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
Defined.
Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
Goal forall n:nat, S n = 1 + n.
Ltac rewrite_S_to_plus_term t :=
match constr:t with
| 1 => constr:1
| (S ?X1) =>
let t1 := rewrite_S_to_plus_term X1 in
constr:(1 + t1)
| (?X1 + ?X2) =>
let t1 := rewrite_S_to_plus_term X1
with t2 := rewrite_S_to_plus_term X2 in
constr:(t1 + t2)
| (?X1 * ?X2) =>
let t1 := rewrite_S_to_plus_term X1
with t2 := rewrite_S_to_plus_term X2 in
constr:(t1 * t2)
| _ => constr:t
end.
Ltac rewrite_S_to_plus :=
match goal with
| |- (?X1 = ?X2) =>
try
let t1 :=
rewrite_S_to_plus_term X1
with t2 := rewrite_S_to_plus_term X2 in
change (t1 = t2) in |- *
| |- (?X1 = ?X2) =>
try
let t1 :=
rewrite_S_to_plus_term X1
with t2 := rewrite_S_to_plus_term X2 in
change (t1 = t2) in |- *
end.
Ltac ring_nat := rewrite_S_to_plus; ring.