Lemma isringmultgtaspartbinophrel (X : ring) (R : hrel X) (is0 : @isbinophrel X R) : (isringmultgt X R) <-> (@ispartbinophrel (ringmultmonoid X) (λ a, R a 0) R). Proof. intros. split. - intro ism. split. + apply (isringmultgttoislringmultgt X is0 ism). + apply (isringmultgttoisrringmultgt X is0 ism). - intro isp. apply (islringmultgttoisringmultgt X (pr1 isp)). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.