Lemma isrigdirprod (X Y : rig) : isrigops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)). Proof. intros. split. - exists (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.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.