Lemma ringismultrcancelableif (X : ring) (x : X) (isr : ∏ y, y * x = 0 → y = 0) : isrcancelable op2 x. Proof. intros. apply (@isinclbetweensets X X). - apply setproperty. - apply setproperty. - intros x1 x2 e. set (e' := maponpaths (λ a, a + ((-x2) * x)) e). simpl in e'. rewrite <- (ringrdistr X _ _ x) in e'. rewrite <- (ringrdistr X _ _ x) in e'. rewrite (ringrinvax1 X x2) in e'. rewrite (ringmult0x X _) in e'. set (e'' := isr (x1 - x2) e'). set (e''' := maponpaths (λ a, a + x2) e''). simpl in e'''. rewrite (ringassoc1 X _ _ x2) in e'''. rewrite (ringlinvax1 X x2) in e'''. rewrite (ringlunax1 X _) in e'''. rewrite (ringrunax1 X _) in e'''. apply e'''. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.