The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 08/09/2016 11:23 AM, Soegtrop, Michael wrote:
> Can someone explain what exactly I need in addition to add this as ring?

Maybe something like:

Require Export Coq.Setoids.Setoid. (* required for [rewrite] *)
Require Export Coq.Classes.Morphisms.

Axiom foo: forall P, P.
Instance i3 : Equivalence (eqmod 3).
apply foo.
Qed.
Instance add3 :
Proper (eqmod 3 ==> eqmod 3 ==> eqmod 3) (addmod 3).
Proof.
apply foo.
Qed.
Instance mul3 :
Proper (eqmod 3 ==> eqmod 3 ==> eqmod 3) (mulmod 3).
Proof.
apply foo.
Qed.
Instance inv3 :
Proper (eqmod 3 ==> eqmod 3) (negmod 3).
Proof.
apply foo.
Qed.


Add Ring ModRing3 : ModRing3.