proposition: Lemma ringismultlcancelableif (X : ring) (x : X) (isl : ∏ y, paths (x * y) 0 -> y = 0) : islcancelable op2 x.
proof: Proof. intros. apply (@isinclbetweensets X X). - apply setproperty. - apply setproperty. - intros x1 x2 e. set (e' := maponpaths (λ a, a + (x * (-x2))) e). simpl in e'. rewrite (pathsinv0 (ringldistr X _ _ x)) in e'. rewrite (pathsinv0 (ringldistr X _ _ x)) in e'. rewrite (ringrinvax1 X x2) in e'. rewrite (ringmultx0 X _) in e'. set (e'' := isl (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'''. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids