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