Lemma CCDRplus_apcompat_r : ∏ x y z : X, x + y ≠ x + z → y ≠ z. Proof. exact (CDRplus_apcompat_r (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)). Qed.
Require Import UniMath.MoreFoundations.Tactics.