Lemma apCDRplus : ∏ x x' y y' : X, x + y ≠ x' + y' → x ≠ x' ∨ y ≠ y'. Proof. exact (isapbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.