Lemma commringismultcancelableif (X : commring) (x : X) (isl : ∏ y, x * y = 0 → y = 0) : iscancelable op2 x. Proof. intros. split. - apply (ringismultlcancelableif X x isl). - assert (isr : ∏ y, y * x = 0 → y = 0). intros y e. rewrite (ringcomm2 X _ _) in e. apply (isl y e). apply (ringismultrcancelableif X x isr). Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.