proposition: Lemma commringismultcancelableif (X : commring) (x : X) (isl : ∏ y, paths (x * y) 0 -> y = 0) : iscancelable op2 x.
proof: Proof. intros. split. - apply (ringismultlcancelableif X x isl). - assert (isr : ∏ y, paths (y * x) 0 -> y = 0). intros y e. rewrite (ringcomm2 X _ _) in e. apply (isl y e). apply (ringismultrcancelableif X x isr). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids