fact: Definition ringfromgt0 (X : ring) {R : hrel X} (is0 : @isbinophrel X R) {x : X} (is : R x 0) : R 0 (- x) := grfromgtunel X is0 is.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids