Lemma iscomptoringdiff (X : rig) {L : hrel X} (is0 : @isbinophrel (rigaddabmonoid X) L) : iscomprelrelfun L (rigtoringrel X is0) (toringdiff X). Proof. apply (iscomptoabgrdiff (rigaddabmonoid X)). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.