proposition: Lemma iscommrigdirprod (X Y : commrig) : iscommrigops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)).
proof: Proof. intros. split with (isrigdirprod X Y). apply (pr2 (isabmonoiddirprod (commrigmultabmonoid X) (commrigmultabmonoid Y))). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids