Lemma CCDRmult_apcompat_l : ∏ x y z : X, y * x ≠ z * x → y ≠ z. Proof. exact (CDRmult_apcompat_l (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.