proposition: Lemma ringismultcancelableif (X : ring) (x : X) (isl : ∏ y, paths (x * y) 0 -> y = 0) (isr : ∏ y, paths (y * x) 0 -> y = 0) : iscancelable op2 x.
proof: Proof. intros. apply (make_dirprod (ringismultlcancelableif X x isl) (ringismultrcancelableif X x isr)). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids