Definition ringfromlt0 (X : ring) {R : hrel X} (is0 : @isbinophrel X R) {x : X} (is : R 0 x) : R (- x) 0 := grfromltunel X is0 is.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.