Definition opposite_rig (X : rig) : rig. Proof. refine (make_setwith2binop (pr1 (pr1rig X)) (pr1 (pr2 (pr1rig X)) ,, λ x y, y * x),, _). unfold op2; cbn; fold (@op1 X) (@op2 X). apply (make_isrigops (rigop1axs X)). - apply make_ismonoidop. * exact (λ x y z, !rigassoc2 _ z y x). * refine (1,, _). exact (rigrunax2 _ ,, riglunax2 _). - exact (rigmultx0 _). - exact (rigmult0x _). - exact (rigrdistr _ ,, rigldistr _). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.