Lemma ringismultcancelableif (X : ring) (x : X) (isl : ∏ y, x * y = 0 → y = 0) (isr : ∏ y, y * x = 0 → y = 0) : iscancelable op2 x. Proof. intros. exact (ringismultlcancelableif X x isl ,, ringismultrcancelableif X x isr). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.