proposition: Lemma isrigdirprod (X Y : rig) : isrigops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)).
proof: Proof. intros. split. - split with (make_dirprod (isabmonoiddirprod (rigaddabmonoid X) (rigaddabmonoid Y)) (ismonoiddirprod (rigmultmonoid X) (rigmultmonoid Y))). simpl. split. + intro xy. unfold setwith2binopdirprod. unfold op1. unfold op2. unfold ismonoiddirprod. unfold unel_is. simpl. apply pathsdirprod. apply (rigmult0x X). apply (rigmult0x Y). + intro xy. unfold setwith2binopdirprod. unfold op1. unfold op2. unfold ismonoiddirprod. unfold unel_is. simpl. apply pathsdirprod. apply (rigmultx0 X). apply (rigmultx0 Y). - split. + intros xy xy' xy''. unfold setwith2binopdirprod. unfold op1. unfold op2. simpl. apply pathsdirprod. apply (rigldistr X). apply (rigldistr Y). + intros xy xy' xy''. unfold setwith2binopdirprod. unfold op1. unfold op2. simpl. apply pathsdirprod. apply (rigrdistr X). apply (rigrdistr Y). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids