Lemma CCDRmultapCCDRzero : ∏ x y : X, x * y ≠ 0 → x ≠ 0 ∧ y ≠ 0. Proof. exact (CDRmultapCDRzero (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.