Definition isinvringmultgt (X : ring) (R : hrel X) : UU := (∏ a b, R (a * b) 0 → R a 0 → R b 0) × (∏ a b, R (a * b) 0 → R b 0 → R a 0).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.