Lemma isinvringmultgtaspartinvbinophrel (X : ring) (R : hrel X) (is0 : @isbinophrel X R) : (isinvringmultgt X R) <-> (@ispartinvbinophrel (ringmultmonoid X) (λ a, R a 0) R). Proof. intros. split. - intro ism. split. + apply (isinvringmultgttoislinvringmultgt X is0 ism). + apply (isinvringmultgttoisrinvringmultgt X is0 ism). - intro isp. apply (islrinvringmultgttoisinvringmultgt X (pr1 isp) (pr2 isp)). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.