proposition: Lemma isringdirprod (X Y : ring) : isringops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)).
proof: Proof. intros. split with (make_dirprod (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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids