Definition commringfracop1int (X : commring) (S : @subabmonoid (ringmultabmonoid X)) : binop (X × S) := λ (x1s1 x2s2 : X × S), pr1 (pr2 x2s2) * pr1 x1s1 + pr1 (pr2 x1s1) * pr1 x2s2 ,, op (pr2 x1s1) (pr2 x2s2).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.