Lemma CFplus_apcompat_l : ∏ x y z : X, y + x ≠ z + x <-> y ≠ z. Proof. intros x y z. split. - exact (CCDRplus_apcompat_l (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) _ _ _). - intros Hap. apply (CCDRplus_apcompat_l (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) (- x)). change ((y + x) + - x ≠ (z + x) + - x). rewrite !isassoc_CFplus, isrinv_CFopp, !isrunit_CFzero_CFplus. exact Hap. Qed.
Require Import UniMath.MoreFoundations.Tactics.