proposition: Lemma CFplus_apcompat_l : ∏ x y z : X, y + x ≠ z + x <-> y ≠ z.
proof: 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.
imports: UniMath.Algebra.DivisionRig UniMath.Algebra.Domains_and_Fields UniMath.Algebra.Apartness UniMath.MoreFoundations.Tactics