Lemma apCCDRmult : ∏ x x' y y' : X, x * y ≠ x' * y' → x ≠ x' ∨ y ≠ y'. Proof. exact (apCDRmult (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.