Definition toringdiff (X : rig) (x : X) : rigtoring X := setquotpr _ (x ,, 0).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.