Definition commrigtocommring (X : commrig) : commring. Proof. exists (rigtoring X). split. - apply (pr2 (rigtoring X)). - apply (commrigtocommringcomm2 X). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.