Lemma CFmult_apcompat_r : ∏ x y z : X, x * y ≠ x * z → y ≠ z. Proof. exact (CCDRmult_apcompat_r (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.