Unset Kernel Term Sharing.

Require Export UniMath.Algebra.DivisionRig.
Require Export UniMath.Algebra.Domains_and_Fields.
Require Export UniMath.Algebra.Apartness.

Require Import UniMath.MoreFoundations.Tactics.

Definition isnonzeroCR (X : rig) (R : tightap X) := R 1%rig 0%rig.
Definition isConstrDivRig (X : rig) (R : tightap X) :=
  isnonzeroCR X R × (∏ x : X, R x 0%rig → multinvpair X x).

Definition ConstructiveDivisionRig :=
  ∑ X : rig,
  ∑ R : tightap X,
        isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op1
      × isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op2
      × isConstrDivRig X R.
Definition ConstructiveDivisionRig_rig : ConstructiveDivisionRig → rig := pr1.
Coercion ConstructiveDivisionRig_rig : ConstructiveDivisionRig >-> rig.
Definition ConstructiveDivisionRig_apsetwith2binop : ConstructiveDivisionRig → apsetwith2binop.
Proof.
  intros X.
  ∃ (pr1 (pr1 (pr1 X)),,(pr1 (pr2 X))).
  split.
  exact (_,,(pr1 (pr2 (pr2 X)))).
  exact (_,,(pr1 (pr2 (pr2 (pr2 X))))).
Defined.

Definition CDRap {X : ConstructiveDivisionRig} : hrel X := λ x y : X, (pr1 (pr2 X)) x y.
Definition CDRzero {X : ConstructiveDivisionRig} : X := 0%rig.
Definition CDRone {X : ConstructiveDivisionRig} : X := 1%rig.
Definition CDRplus {X : ConstructiveDivisionRig} : binop X := λ x y : X, op1 (X := ConstructiveDivisionRig_apsetwith2binop X) x y.
Definition CDRmult {X : ConstructiveDivisionRig} : binop X := λ x y : X, op2 (X := ConstructiveDivisionRig_apsetwith2binop X) x y.

Declare Scope CDR_scope.
Delimit Scope CDR_scope with CDR.
Local Open Scope CDR_scope.

Notation "x ≠ y" := (CDRap x y) (at level 70, no associativity) : CDR_scope.
Notation "0" := CDRzero : CDR_scope.
Notation "1" := CDRone : CDR_scope.
Notation "x + y" := (CDRplus x y) : CDR_scope.
Notation "x * y" := (CDRmult x y) : CDR_scope.

Definition CDRinv {X : ConstructiveDivisionRig} (x : X) (Hx0 : x ≠ 0) : X :=
  (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 X)))) x Hx0)).
Definition CDRdiv {X : ConstructiveDivisionRig} (x y : X) (Hy0 : y ≠ 0) : X :=
  CDRmult x (CDRinv y Hy0).

Section CDR_pty.

Context {X : ConstructiveDivisionRig}.

Lemma isirrefl_CDRap :
  ∏ x : X, ¬ (x ≠ x).
Proof.
  exact (pr1 (pr1 (pr2 (pr1 (pr2 X))))).
Qed.
Lemma issymm_CDRap :
  ∏ x y : X, x ≠ y → y ≠ x.
Proof.
  exact (pr1 (pr2 (pr1 (pr2 (pr1 (pr2 X)))))).
Qed.
Lemma iscotrans_CDRap :
  ∏ x y z : X, x ≠ z → x ≠ y ∨ y ≠ z.
Proof.
  exact (pr2 (pr2 (pr1 (pr2 (pr1 (pr2 X)))))).
Qed.
Lemma istight_CDRap :
  ∏ x y : X, ¬ (x ≠ y) → x = y.
Proof.
  exact (pr2 (pr2 (pr1 (pr2 X)))).
Qed.

Lemma isnonzeroCDR : (1 : X) ≠ (0 : X).
Proof.
  exact (pr1 (pr2 (pr2 (pr2 (pr2 X))))).
Qed.

Lemma islunit_CDRzero_CDRplus :
  ∏ x : X, 0 + x = x.
Proof.
  now apply riglunax1.
Qed.
Lemma isrunit_CDRzero_CDRplus :
  ∏ x : X, x + 0 = x.
Proof.
  now apply rigrunax1.
Qed.
Lemma isassoc_CDRplus :
  ∏ x y z : X, x + y + z = x + (y + z).
Proof.
  now apply rigassoc1.
Qed.
Lemma iscomm_CDRplus :
  ∏ x y : X, x + y = y + x.
Proof.
  now apply rigcomm1.
Qed.
Lemma islunit_CDRone_CDRmult :
  ∏ x : X, 1 × x = x.
Proof.
  now apply riglunax2.
Qed.
Lemma isrunit_CDRone_CDRmult :
  ∏ x : X, x × 1 = x.
Proof.
  now apply rigrunax2.
Qed.
Lemma isassoc_CDRmult :
  ∏ x y z : X, x × y × z = x × (y × z).
Proof.
  now apply rigassoc2.
Qed.
Lemma islinv_CDRinv :
  ∏ (x : X) (Hx0 : x ≠ (0 : X)),
    (CDRinv x Hx0) × x = 1.
Proof.
  intros x Hx0.
  apply (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 X)))) x Hx0))).
Qed.
Lemma isrinv_CDRinv :
  ∏ (x : X) (Hx0 : x ≠ (0 : X)),
    x × (CDRinv x Hx0) = 1.
Proof.
  intros x Hx0.
  apply (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 X)))) x Hx0))).
Qed.
Lemma islabsorb_CDRzero_CDRmult :
  ∏ x : X, 0 × x = 0.
Proof.
  now apply rigmult0x.
Qed.
Lemma israbsorb_CDRzero_CDRmult :
  ∏ x : X, x × 0 = 0.
Proof.
  now apply rigmultx0.
Qed.
Lemma isldistr_CDRplus_CDRmult :
  ∏ x y z : X, z × (x + y) = z × x + z × y.
Proof.
  now apply rigdistraxs.
Qed.

Lemma apCDRplus :
  ∏ x x' y y' : X,
    x + y ≠ x' + y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (isapbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X)).
Qed.
Lemma CDRplus_apcompat_l :
  ∏ x y z : X, y + x ≠ z + x → y ≠ z.
Proof.
  intros x y z.
  exact (islapbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X) _ _ _).
Qed.
Lemma CDRplus_apcompat_r :
  ∏ x y z : X, x + y ≠ x + z → y ≠ z.
Proof.
  exact (israpbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X)).
Qed.

Lemma apCDRmult :
  ∏ x x' y y' : X,
    x × y ≠ x' × y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (isapbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X)).
Qed.
Lemma CDRmult_apcompat_l :
  ∏ x y z : X, y × x ≠ z × x → y ≠ z.
Proof.
  intros x y z.
  exact (islapbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X) _ _ _).
Qed.
Lemma CDRmult_apcompat_l' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → y × x ≠ z × x.
Proof.
  intros x y z Hx Hap.
  refine (CDRmult_apcompat_l (CDRinv x Hx) _ _ _).
  rewrite !isassoc_CDRmult, isrinv_CDRinv, !isrunit_CDRone_CDRmult.
  exact Hap.
Qed.
Lemma CDRmult_apcompat_r :
  ∏ x y z : X, x × y ≠ x × z → y ≠ z.
Proof.
  exact (israpbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X)).
Qed.
Lemma CDRmult_apcompat_r' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → x × y ≠ x × z.
Proof.
  intros x y z Hx Hap.
  refine (CDRmult_apcompat_r (CDRinv x Hx) _ _ _).
  rewrite <- !isassoc_CDRmult, islinv_CDRinv, !islunit_CDRone_CDRmult.
  exact Hap.
Qed.

Lemma CDRmultapCDRzero :
  ∏ x y : X, x × y ≠ 0 → x ≠ 0 ∧ y ≠ 0.
Proof.
  intros x y Hmult.
  split.
  - apply CDRmult_apcompat_l with y.
    rewrite islabsorb_CDRzero_CDRmult.
    exact Hmult.
  - apply CDRmult_apcompat_r with x.
    rewrite israbsorb_CDRzero_CDRmult.
    exact Hmult.
Qed.

Close Scope CDR_scope.

End CDR_pty.

Definition ConstructiveCommutativeDivisionRig :=
  ∑ X : commrig,
  ∑ R : tightap X,
        isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op1
      × isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op2
      × isConstrDivRig X R.
Definition ConstructiveCommutativeDivisionRig_commrig :
  ConstructiveCommutativeDivisionRig → commrig := pr1.
Coercion ConstructiveCommutativeDivisionRig_commrig :
  ConstructiveCommutativeDivisionRig >-> commrig.

Definition ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig :
  ConstructiveCommutativeDivisionRig → ConstructiveDivisionRig :=
  λ X, (pr1 (pr1 X),,pr1 (pr2 (pr1 X))) ,, (pr2 X).
Coercion ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig :
  ConstructiveCommutativeDivisionRig >-> ConstructiveDivisionRig.

Definition CCDRap {X : ConstructiveCommutativeDivisionRig} : hrel X := λ x y : X, CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X) x y.
Definition CCDRzero {X : ConstructiveCommutativeDivisionRig} : X := 0%rig.
Definition CCDRone {X : ConstructiveCommutativeDivisionRig} : X := 1%rig.
Definition CCDRplus {X : ConstructiveCommutativeDivisionRig} : binop X := λ x y : X, CDRplus (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X) x y.
Definition CCDRmult {X : ConstructiveCommutativeDivisionRig} : binop X := λ x y : X, CDRmult (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X) x y.

Declare Scope CCDR_scope.
Delimit Scope CCDR_scope with CCDR.
Local Open Scope CCDR_scope.

Notation "x ≠ y" := (CCDRap x y) (at level 70, no associativity) : CCDR_scope.
Notation "0" := CCDRzero : CCDR_scope.
Notation "1" := CCDRone : CCDR_scope.
Notation "x + y" := (CCDRplus x y) : CCDR_scope.
Notation "x * y" := (CCDRmult x y) : CCDR_scope.

Definition CCDRinv {X : ConstructiveCommutativeDivisionRig} (x : X) (Hx0 : x ≠ CCDRzero) : X :=
  CDRinv (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X) x Hx0.
Definition CCDRdiv {X : ConstructiveCommutativeDivisionRig} (x y : X) (Hy0 : y ≠ CCDRzero) : X :=
  CCDRmult x (CCDRinv y Hy0).

Section CCDR_pty.

Context {X : ConstructiveCommutativeDivisionRig}.

Lemma isirrefl_CCDRap :
  ∏ x : X, ¬ (x ≠ x).
Proof.
  exact (isirrefl_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma issymm_CCDRap :
  ∏ x y : X, x ≠ y → y ≠ x.
Proof.
  exact (issymm_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma iscotrans_CCDRap :
  ∏ x y z : X, x ≠ z → x ≠ y ∨ y ≠ z.
Proof.
  exact (iscotrans_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma istight_CCDRap :
  ∏ x y : X, ¬ (x ≠ y) → x = y.
Proof.
  exact (istight_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.

Lemma isnonzeroCCDR : (1 : X) ≠ (0 : X).
Proof.
  exact isnonzeroCDR.
Qed.

Lemma islunit_CCDRzero_CCDRplus :
  ∏ x : X, 0 + x = x.
Proof.
  now apply riglunax1.
Qed.
Lemma isrunit_CCDRzero_CCDRplus :
  ∏ x : X, x + 0 = x.
Proof.
  now apply rigrunax1.
Qed.
Lemma isassoc_CCDRplus :
  ∏ x y z : X, x + y + z = x + (y + z).
Proof.
  now apply rigassoc1.
Qed.
Lemma iscomm_CCDRplus :
  ∏ x y : X, x + y = y + x.
Proof.
  now apply rigcomm1.
Qed.
Lemma islunit_CCDRone_CCDRmult :
  ∏ x : X, 1 × x = x.
Proof.
  now apply riglunax2.
Qed.
Lemma isrunit_CCDRone_CCDRmult :
  ∏ x : X, x × 1 = x.
Proof.
  now apply rigrunax2.
Qed.
Lemma isassoc_CCDRmult :
  ∏ x y z : X, x × y × z = x × (y × z).
Proof.
  now apply rigassoc2.
Qed.
Lemma iscomm_CCDRmult :
  ∏ x y : X, x × y = y × x.
Proof.
  now apply rigcomm2.
Qed.
Lemma islinv_CCDRinv :
  ∏ (x : X) (Hx0 : x ≠ (0 : X)),
    (CDRinv (X := X) x Hx0) × x = 1.
Proof.
  exact (islinv_CDRinv (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma isrinv_CCDRinv :
  ∏ (x : X) (Hx0 : x ≠ (0 : X)),
    x × (CDRinv (X := X) x Hx0) = 1.
Proof.
  exact (isrinv_CDRinv (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma islabsorb_CCDRzero_CCDRmult :
  ∏ x : X, 0 × x = 0.
Proof.
  now apply rigmult0x.
Qed.
Lemma israbsorb_CCDRzero_CCDRmult :
  ∏ x : X, x × 0 = 0.
Proof.
  now apply rigmultx0.
Qed.
Lemma isldistr_CCDRplus_CCDRmult :
  ∏ x y z : X, z × (x + y) = z × x + z × y.
Proof.
  now apply rigdistraxs.
Qed.
Lemma isrdistr_CCDRplus_CCDRmult :
  ∏ x y z : X, (x + y) × z = x × z + y × z.
Proof.
  intros x y z.
  rewrite !(iscomm_CCDRmult _ z).
  now apply rigdistraxs.
Qed.

Lemma apCCDRplus :
  ∏ x x' y y' : X,
    x + y ≠ x' + y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (apCDRplus (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRplus_apcompat_l :
  ∏ x y z : X, y + x ≠ z + x → y ≠ z.
Proof.
  exact (CDRplus_apcompat_l (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRplus_apcompat_r :
  ∏ x y z : X, x + y ≠ x + z → y ≠ z.
Proof.
  exact (CDRplus_apcompat_r (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.

Lemma apCCDRmult :
  ∏ x x' y y' : X,
    x × y ≠ x' × y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (apCDRmult (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRmult_apcompat_l :
  ∏ x y z : X, y × x ≠ z × x → y ≠ z.
Proof.
  exact (CDRmult_apcompat_l (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRmult_apcompat_l' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → y × x ≠ z × x.
Proof.
  exact (CDRmult_apcompat_l' (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRmult_apcompat_r :
  ∏ x y z : X, x × y ≠ x × z → y ≠ z.
Proof.
  exact (CDRmult_apcompat_r (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.
Lemma CCDRmult_apcompat_r' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → x × y ≠ x × z.
Proof.
  exact (CDRmult_apcompat_r' (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.

Lemma CCDRmultapCCDRzero :
  ∏ x y : X, x × y ≠ 0 → x ≠ 0 ∧ y ≠ 0.
Proof.
  exact (CDRmultapCDRzero (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).
Qed.

Close Scope CCDR_scope.

End CCDR_pty.

Definition ConstructiveField :=
  ∑ X : commring,
  ∑ R : tightap X,
        isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op1
      × isapbinop (X := (pr1 (pr1 X)) ,, R) BinaryOperations.op2
      × isConstrDivRig X R.
Definition ConstructiveField_commring :
  ConstructiveField → commring := pr1.
Coercion ConstructiveField_commring :
  ConstructiveField >-> commring.
Definition ConstructiveField_ConstructiveCommutativeDivisionRig :
  ConstructiveField → ConstructiveCommutativeDivisionRig :=
  λ X, (commringtocommrig (pr1 X)) ,, (pr2 X).
Coercion ConstructiveField_ConstructiveCommutativeDivisionRig :
  ConstructiveField >-> ConstructiveCommutativeDivisionRig.

Definition CFap {X : ConstructiveField} : hrel X := λ x y : X, CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) x y.
Definition CFzero {X : ConstructiveField} : X := 0%ring.
Definition CFone {X : ConstructiveField} : X := 1%ring.
Definition CFplus {X : ConstructiveField} : binop X := λ x y : X, CCDRplus (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) x y.
Definition CFopp {X : ConstructiveField} : unop X := λ x : X, (- x)%ring.
Definition CFminus {X : ConstructiveField} : binop X := λ x y : X, CFplus x (CFopp y).
Definition CFmult {X : ConstructiveField} : binop X := λ x y : X, CCDRmult (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) x y.

Declare Scope CF_scope.
Delimit Scope CF_scope with CF.
Local Open Scope CF_scope.

Notation "x ≠ y" := (CFap x y) (at level 70, no associativity) : CF_scope.
Notation "0" := CFzero : CF_scope.
Notation "1" := CFone : CF_scope.
Notation "x + y" := (CFplus x y) : CF_scope.
Notation "- x" := (CFopp x) : CF_scope.
Notation "x - y" := (CFminus x y) : CF_scope.
Notation "x * y" := (CFmult x y) : CF_scope.

Definition CFinv {X : ConstructiveField} (x : X) (Hx0 : x ≠ CFzero) : X :=
  CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X) x Hx0.
Definition CFdiv {X : ConstructiveField} (x y : X) (Hy0 : y ≠ CFzero) : X :=
  CFmult x (CFinv y Hy0).

Section CF_pty.

Context {X : ConstructiveField}.

Lemma isirrefl_CFap :
  ∏ x : X, ¬ (x ≠ x).
Proof.
  exact (isirrefl_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma issymm_CFap :
  ∏ x y : X, x ≠ y → y ≠ x.
Proof.
  exact (issymm_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma iscotrans_CFap :
  ∏ x y z : X, x ≠ z → x ≠ y ∨ y ≠ z.
Proof.
  exact (iscotrans_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma istight_CFap :
  ∏ x y : X, ¬ (x ≠ y) → x = y.
Proof.
  exact (istight_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.

Lemma isnonzeroCF : (1 : X) ≠ (0 : X).
Proof.
  exact (isnonzeroCCDR (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.

Lemma islunit_CFzero_CFplus :
  ∏ x : X, 0 + x = x.
Proof.
  now apply ringlunax1.
Qed.
Lemma isrunit_CFzero_CFplus :
  ∏ x : X, x + 0 = x.
Proof.
  now apply ringrunax1.
Qed.
Lemma isassoc_CFplus :
  ∏ x y z : X, x + y + z = x + (y + z).
Proof.
  now apply ringassoc1.
Qed.
Lemma islinv_CFopp :
  ∏ x : X, - x + x = 0.
Proof.
  now apply ringlinvax1.
Qed.
Lemma isrinv_CFopp :
  ∏ x : X, x + - x = 0.
Proof.
  now apply ringrinvax1.
Qed.

Lemma iscomm_CFplus :
  ∏ x y : X, x + y = y + x.
Proof.
  now apply ringcomm1.
Qed.
Lemma islunit_CFone_CFmult :
  ∏ x : X, 1 × x = x.
Proof.
  now apply ringlunax2.
Qed.
Lemma isrunit_CFone_CFmult :
  ∏ x : X, x × 1 = x.
Proof.
  now apply ringrunax2.
Qed.
Lemma isassoc_CFmult :
  ∏ x y z : X, x × y × z = x × (y × z).
Proof.
  now apply ringassoc2.
Qed.
Lemma iscomm_CFmult :
  ∏ x y : X, x × y = y × x.
Proof.
  now apply ringcomm2.
Qed.
Lemma islinv_CFinv :
  ∏ (x : X) (Hx0 : x ≠ 0),
    (CFinv x Hx0) × x = 1.
Proof.
  exact (islinv_CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma isrinv_CFinv :
  ∏ (x : X) (Hx0 : x ≠ 0),
    x × (CFinv x Hx0) = 1.
Proof.
  exact (isrinv_CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma islabsorb_CFzero_CFmult :
  ∏ x : X, 0 × x = 0.
Proof.
  now apply ringmult0x.
Qed.
Lemma israbsorb_CFzero_CFmult :
  ∏ x : X, x × 0 = 0.
Proof.
  now apply ringmultx0.
Qed.
Lemma isldistr_CFplus_CFmult :
  ∏ x y z : X, z × (x + y) = z × x + z × y.
Proof.
  now apply ringdistraxs.
Qed.
Lemma isrdistr_CFplus_CFmult :
  ∏ x y z : X, (x + y) × z = x × z + y × z.
Proof.
  intros.
  rewrite !(iscomm_CFmult _ z).
  now apply isldistr_CFplus_CFmult.
Qed.

Lemma apCFplus :
  ∏ x x' y y' : X,
    x + y ≠ x' + y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (apCCDRplus (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
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.
Lemma CFplus_apcompat_r :
  ∏ x y z : X, x + y ≠ x + z ↔ y ≠ z.
Proof.
  intros x y z.
  rewrite !(iscomm_CFplus x).
  now apply CFplus_apcompat_l.
Qed.

Lemma apCFmult :
  ∏ x x' y y' : X,
    x × y ≠ x' × y' → x ≠ x' ∨ y ≠ y'.
Proof.
  exact (apCCDRmult (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma CFmult_apcompat_l :
  ∏ x y z : X, y × x ≠ z × x → y ≠ z.
Proof.
  exact (CCDRmult_apcompat_l (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma CFmult_apcompat_l' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → y × x ≠ z × x.
Proof.
  exact (CCDRmult_apcompat_l' (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma CFmult_apcompat_r :
  ∏ x y z : X, x × y ≠ x × z → y ≠ z.
Proof.
  exact (CCDRmult_apcompat_r (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.
Lemma CFmult_apcompat_r' :
  ∏ x y z : X, x ≠ 0 → y ≠ z → x × y ≠ x × z.
Proof.
  exact (CCDRmult_apcompat_r' (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.

Lemma CFmultapCFzero :
  ∏ x y : X, x × y ≠ 0 → x ≠ 0 ∧ y ≠ 0.
Proof.
  exact (CCDRmultapCCDRzero (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).
Qed.

End CF_pty.

Close Scope CF_scope.