proposition: Lemma isbinop2funtoringdiff (X : rig) : @isbinopfun (rigmultmonoid X) (ringmultmonoid (rigtoring X)) (toringdiff X).
proof: Proof. intros. unfold isbinopfun. intros x x'. change (paths (setquotpr _ (make_dirprod (x * x') 0)) (setquotpr (eqrelrigtoring X) (rigtoringop2int X (make_dirprod x 0) (make_dirprod x' 0)))). apply (maponpaths (setquotpr _)). unfold rigtoringop2int. simpl. apply pathsdirprod. - rewrite (rigmultx0 X _). rewrite (rigrunax1 X _). apply idpath. - rewrite (rigmult0x X _). rewrite (rigmultx0 X _). rewrite (rigrunax1 X _). apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids