Definition isdecrigtoringrel (X : rig) {R : hrel X} (is : @isbinophrel (rigaddabmonoid X) R) (is' : @isinvbinophrel (rigaddabmonoid X) R) (isd : isdecrel R) : isdecrel (rigtoringrel X is). Proof. intros. apply (isdecabgrdiffrel (rigaddabmonoid X) is is' isd). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.