Lemma isringdirprod (X Y : ring) : isringops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)). Proof. intros. exists (isabgrdirprod X Y ,, ismonoiddirprod (ringmultmonoid X) (ringmultmonoid Y)). simpl. split. - intros xy xy' xy''. unfold setwith2binopdirprod. unfold op1. unfold op2. simpl. apply pathsdirprod. + apply (ringldistr X). + apply (ringldistr Y). - intros xy xy' xy''. unfold setwith2binopdirprod. unfold op1. unfold op2. simpl. apply pathsdirprod. + apply (ringrdistr X). + apply (ringrdistr Y). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.