Lemma iscommringdirprod (X Y : commring) : iscommringops (@op1 (setwith2binopdirprod X Y)) (@op2 (setwith2binopdirprod X Y)). Proof. intros. exists (isringdirprod X Y). apply (pr2 (isabmonoiddirprod (ringmultabmonoid X) (ringmultabmonoid Y))). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.