Lemma isbinop1funtoringdiff (X : rig) : @isbinopfun (rigaddabmonoid X) (rigtoring X) (toringdiff X). Proof. intros. unfold isbinopfun. intros x x'. apply (isbinopfuntoabgrdiff (rigaddabmonoid X) x x'). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.