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. intros. split. - intros a b rab ra. rewrite <- (ringmultx0 X a) in rab. apply (isl _ _ _ ra rab). - intros a b rab rb. rewrite <- (ringmult0x X b) in rab. apply (isr _ _ _ rb rab). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.