# Library Coq.setoid_ring.Ring_equiv

Require Import Setoid_ring_theory.
Require Import LegacyRing_theory.
Require Import Ring_theory.
Section Old2New.
Variable A : Type.
Variable Aplus : A -> A -> A.
Variable Amult : A -> A -> A.
Variable Aone : A.
Variable Azero : A.
Variable Aopp : A -> A.
Variable Aeq : A -> A -> bool.
Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
Let Aminus := fun x y => Aplus x (Aopp y).
Lemma ring_equiv1 :
ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
End Old2New.
Section New2OldRing.
Variable R : Type.
Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
Variable reqb : R -> R -> bool.
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
Lemma ring_equiv2 :
Ring_Theory radd rmul rI rO ropp reqb.
Definition default_eqb : R -> R -> bool := fun x y => false.
Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
End New2OldRing.
Section New2OldSemiRing.
Variable R : Type.
Variable (rO rI : R) (radd rmul: R->R->R).
Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
Variable reqb : R -> R -> bool.
Variable reqb_ok : forall x y, reqb x y = true -> x = y.
Lemma sring_equiv2 :
Semi_Ring_Theory radd rmul rI rO reqb.
End New2OldSemiRing.