proposition: Lemma islrinvringmultgttoisinvringmultgt (X : ring) {R : hrel X} (isl : ∏ a b c : X, R c 0 -> R (c * a) (c * b) -> R a b) (isr : ∏ a b c : X, R c 0 -> R (a * c) (b * c) -> R a b) : isinvringmultgt X R.
proof: Proof. intros. split. - intros a b rab ra. rewrite (pathsinv0 (ringmultx0 X a)) in rab. apply (isl _ _ _ ra rab). - intros a b rab rb. rewrite (pathsinv0 (ringmult0x X b)) in rab. apply (isr _ _ _ rb rab). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids