Definition rigtoringop2int (X : rig) : binop (X × X) := λ xx xx' : X × X, pr1 xx * pr1 xx' + pr2 xx * pr2 xx' ,, pr1 xx * pr2 xx' + pr2 xx * pr1 xx'.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.