fact: Definition commringdirprod (X Y : commring) : commring := make_commring (setwith2binopdirprod X Y) (iscommringdirprod X Y).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids