Definition iso_commring_opposite (X : commring) : rigiso X (opposite_commring X) := iso_commrig_opposite X.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.