proposition: Lemma isinvringmultgtaspartinvbinophrel (X : ring) (R : hrel X) (is0 : @isbinophrel X R) : (isinvringmultgt X R) <-> (@ispartinvbinophrel (ringmultmonoid X) (λ a, R a 0) R).
proof: 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.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids