Library UniMath.Algebra.ConstructiveStructures

Definition of appartness relationConstructive Algebraic Structures

Catherine Lelay. Sep. 2015

Unset Kernel Term Sharing.

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

Require Import UniMath.MoreFoundations.Tactics.

Predicats in a rig with a tight appartness relation

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).

Constructive rig with division

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.
Show proof.

  intros X.
  exists (pr1 (pr1 (pr1 X)),,(pr1 (pr2 X))).
  split.
  exact (_,,(pr1 (pr2 (pr2 X)))).
  exact (_,,(pr1 (pr2 (pr2 (pr2 X))))).

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.

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).

Lemmas

Section CDR_pty.

Context {X : ConstructiveDivisionRig}.

Lemma isirrefl_CDRap :
∏ x : X, ¬ (x ≠ x).
Show proof.

exact (pr1 (pr1 (pr2 (pr1 (pr2 X))))).

Lemma issymm_CDRap :
∏ x y : X, x ≠ y -> y ≠ x.
Show proof.

exact (pr1 (pr2 (pr1 (pr2 (pr1 (pr2 X)))))).

Lemma iscotrans_CDRap :
∏ x y z : X, x ≠ z -> x ≠ y ∨ y ≠ z.
Show proof.

exact (pr2 (pr2 (pr1 (pr2 (pr1 (pr2 X)))))).

Lemma istight_CDRap :
∏ x y : X, ¬ (x ≠ y) -> x = y.
Show proof.

exact (pr2 (pr2 (pr1 (pr2 X)))).

Lemma isnonzeroCDR : (1 : X) ≠ (0 : X).
Show proof.

exact (pr1 (pr2 (pr2 (pr2 (pr2 X))))).

Lemma islunit_CDRzero_CDRplus :
∏ x : X, 0 + x = x.
Show proof.

now apply riglunax1.

Lemma isrunit_CDRzero_CDRplus :
∏ x : X, x + 0 = x.
Show proof.

now apply rigrunax1.

Lemma isassoc_CDRplus :
∏ x y z : X, x + y + z = x + (y + z).
Show proof.

now apply rigassoc1.

Lemma iscomm_CDRplus :
∏ x y : X, x + y = y + x.
Show proof.

now apply rigcomm1.

Lemma islunit_CDRone_CDRmult :
∏ x : X, 1 * x = x.
Show proof.

now apply riglunax2.

Lemma isrunit_CDRone_CDRmult :
∏ x : X, x * 1 = x.
Show proof.

now apply rigrunax2.

Lemma isassoc_CDRmult :
∏ x y z : X, x * y * z = x * (y * z).
Show proof.

now apply rigassoc2.

Lemma islinv_CDRinv :
∏ (x : X) (Hx0 : x ≠ (0 : X)),
(CDRinv x Hx0) * x = 1.
Show proof.

intros x Hx0.
apply (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 X)))) x Hx0))).

Lemma isrinv_CDRinv :
∏ (x : X) (Hx0 : x ≠ (0 : X)),
x * (CDRinv x Hx0) = 1.
Show proof.

intros x Hx0.
apply (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 X)))) x Hx0))).

Lemma islabsorb_CDRzero_CDRmult :
∏ x : X, 0 * x = 0.
Show proof.

now apply rigmult0x.

Lemma israbsorb_CDRzero_CDRmult :
∏ x : X, x * 0 = 0.
Show proof.

now apply rigmultx0.

Lemma isldistr_CDRplus_CDRmult :
∏ x y z : X, z * (x + y) = z * x + z * y.
Show proof.

now apply rigdistraxs.

Lemma apCDRplus :
∏ x x' y y' : X,
x + y ≠ x' + y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (isapbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X)).

Lemma CDRplus_apcompat_l :
∏ x y z : X, y + x ≠ z + x -> y ≠ z.
Show proof.

intros x y z.
exact (islapbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X) _ _ _).

Lemma CDRplus_apcompat_r :
∏ x y z : X, x + y ≠ x + z -> y ≠ z.
Show proof.

exact (israpbinop_op1 (X := ConstructiveDivisionRig_apsetwith2binop X)).

Lemma apCDRmult :
∏ x x' y y' : X,
x * y ≠ x' * y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (isapbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X)).

Lemma CDRmult_apcompat_l :
∏ x y z : X, y * x ≠ z * x -> y ≠ z.
Show proof.

intros x y z.
exact (islapbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X) _ _ _).

Lemma CDRmult_apcompat_l' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> y * x ≠ z * x.
Show proof.

  intros x y z Hx Hap.
  refine (CDRmult_apcompat_l (CDRinv x Hx) _ _ _).
  rewrite !isassoc_CDRmult, isrinv_CDRinv, !isrunit_CDRone_CDRmult.
  exact Hap.

Lemma CDRmult_apcompat_r :
∏ x y z : X, x * y ≠ x * z -> y ≠ z.
Show proof.

exact (israpbinop_op2 (X := ConstructiveDivisionRig_apsetwith2binop X)).

Lemma CDRmult_apcompat_r' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> x * y ≠ x * z.
Show proof.

  intros x y z Hx Hap.
  refine (CDRmult_apcompat_r (CDRinv x Hx) _ _ _).
  rewrite <- !isassoc_CDRmult, islinv_CDRinv, !islunit_CDRone_CDRmult.
  exact Hap.

Lemma CDRmultapCDRzero :
∏ x y : X, x * y ≠ 0 -> x ≠ 0 ∧ y ≠ 0.
Show 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.

Close Scope CDR_scope.

End CDR_pty.

Constructive commutative rig with division

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.

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).

Lemmas

Section CCDR_pty.

Context {X : ConstructiveCommutativeDivisionRig}.

Lemma isirrefl_CCDRap :
∏ x : X, ¬ (x ≠ x).
Show proof.

exact (isirrefl_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma issymm_CCDRap :
∏ x y : X, x ≠ y -> y ≠ x.
Show proof.

exact (issymm_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma iscotrans_CCDRap :
∏ x y z : X, x ≠ z -> x ≠ y ∨ y ≠ z.
Show proof.

exact (iscotrans_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma istight_CCDRap :
∏ x y : X, ¬ (x ≠ y) -> x = y.
Show proof.

exact (istight_CDRap (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma isnonzeroCCDR : (1 : X) ≠ (0 : X).
Show proof.

exact isnonzeroCDR.

Lemma islunit_CCDRzero_CCDRplus :
∏ x : X, 0 + x = x.
Show proof.

now apply riglunax1.

Lemma isrunit_CCDRzero_CCDRplus :
∏ x : X, x + 0 = x.
Show proof.

now apply rigrunax1.

Lemma isassoc_CCDRplus :
∏ x y z : X, x + y + z = x + (y + z).
Show proof.

now apply rigassoc1.

Lemma iscomm_CCDRplus :
∏ x y : X, x + y = y + x.
Show proof.

now apply rigcomm1.

Lemma islunit_CCDRone_CCDRmult :
∏ x : X, 1 * x = x.
Show proof.

now apply riglunax2.

Lemma isrunit_CCDRone_CCDRmult :
∏ x : X, x * 1 = x.
Show proof.

now apply rigrunax2.

Lemma isassoc_CCDRmult :
∏ x y z : X, x * y * z = x * (y * z).
Show proof.

now apply rigassoc2.

Lemma iscomm_CCDRmult :
∏ x y : X, x * y = y * x.
Show proof.

now apply rigcomm2.

Lemma islinv_CCDRinv :
∏ (x : X) (Hx0 : x ≠ (0 : X)),
(CDRinv (X := X) x Hx0) * x = 1.
Show proof.

exact (islinv_CDRinv (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma isrinv_CCDRinv :
∏ (x : X) (Hx0 : x ≠ (0 : X)),
x * (CDRinv (X := X) x Hx0) = 1.
Show proof.

exact (isrinv_CDRinv (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma islabsorb_CCDRzero_CCDRmult :
∏ x : X, 0 * x = 0.
Show proof.

now apply rigmult0x.

Lemma israbsorb_CCDRzero_CCDRmult :
∏ x : X, x * 0 = 0.
Show proof.

now apply rigmultx0.

Lemma isldistr_CCDRplus_CCDRmult :
∏ x y z : X, z * (x + y) = z * x + z * y.
Show proof.

now apply rigdistraxs.

Lemma isrdistr_CCDRplus_CCDRmult :
∏ x y z : X, (x + y) * z = x * z + y * z.
Show proof.

  intros x y z.
  rewrite !(iscomm_CCDRmult _ z).
  now apply rigdistraxs.

Lemma apCCDRplus :
∏ x x' y y' : X,
x + y ≠ x' + y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (apCDRplus (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRplus_apcompat_l :
∏ x y z : X, y + x ≠ z + x -> y ≠ z.
Show proof.

exact (CDRplus_apcompat_l (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRplus_apcompat_r :
∏ x y z : X, x + y ≠ x + z -> y ≠ z.
Show proof.

exact (CDRplus_apcompat_r (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma apCCDRmult :
∏ x x' y y' : X,
x * y ≠ x' * y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (apCDRmult (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRmult_apcompat_l :
∏ x y z : X, y * x ≠ z * x -> y ≠ z.
Show proof.

exact (CDRmult_apcompat_l (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRmult_apcompat_l' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> y * x ≠ z * x.
Show proof.

exact (CDRmult_apcompat_l' (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRmult_apcompat_r :
∏ x y z : X, x * y ≠ x * z -> y ≠ z.
Show proof.

exact (CDRmult_apcompat_r (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRmult_apcompat_r' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> x * y ≠ x * z.
Show proof.

exact (CDRmult_apcompat_r' (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Lemma CCDRmultapCCDRzero :
∏ x y : X, x * y ≠ 0 -> x ≠ 0 ∧ y ≠ 0.
Show proof.

exact (CDRmultapCDRzero (X := ConstructiveCommutativeDivisionRig_ConstructiveDivisionRig X)).

Close Scope CCDR_scope.

End CCDR_pty.

Constructive Field

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.

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).

Lemmas

Section CF_pty.

Context {X : ConstructiveField}.

Lemma isirrefl_CFap :
∏ x : X, ¬ (x ≠ x).
Show proof.

exact (isirrefl_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma issymm_CFap :
∏ x y : X, x ≠ y -> y ≠ x.
Show proof.

exact (issymm_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma iscotrans_CFap :
∏ x y z : X, x ≠ z -> x ≠ y ∨ y ≠ z.
Show proof.

exact (iscotrans_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma istight_CFap :
∏ x y : X, ¬ (x ≠ y) -> x = y.
Show proof.

exact (istight_CCDRap (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma isnonzeroCF : (1 : X) ≠ (0 : X).
Show proof.

exact (isnonzeroCCDR (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma islunit_CFzero_CFplus :
∏ x : X, 0 + x = x.
Show proof.

now apply ringlunax1.

Lemma isrunit_CFzero_CFplus :
∏ x : X, x + 0 = x.
Show proof.

now apply ringrunax1.

Lemma isassoc_CFplus :
∏ x y z : X, x + y + z = x + (y + z).
Show proof.

now apply ringassoc1.

Lemma islinv_CFopp :
∏ x : X, - x + x = 0.
Show proof.

now apply ringlinvax1.

Lemma isrinv_CFopp :
∏ x : X, x + - x = 0.
Show proof.

now apply ringrinvax1.

Lemma iscomm_CFplus :
∏ x y : X, x + y = y + x.
Show proof.

now apply ringcomm1.

Lemma islunit_CFone_CFmult :
∏ x : X, 1 * x = x.
Show proof.

now apply ringlunax2.

Lemma isrunit_CFone_CFmult :
∏ x : X, x * 1 = x.
Show proof.

now apply ringrunax2.

Lemma isassoc_CFmult :
∏ x y z : X, x * y * z = x * (y * z).
Show proof.

now apply ringassoc2.

Lemma iscomm_CFmult :
∏ x y : X, x * y = y * x.
Show proof.

now apply ringcomm2.

Lemma islinv_CFinv :
∏ (x : X) (Hx0 : x ≠ 0),
(CFinv x Hx0) * x = 1.
Show proof.

exact (islinv_CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma isrinv_CFinv :
∏ (x : X) (Hx0 : x ≠ 0),
x * (CFinv x Hx0) = 1.
Show proof.

exact (isrinv_CCDRinv (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma islabsorb_CFzero_CFmult :
∏ x : X, 0 * x = 0.
Show proof.

now apply ringmult0x.

Lemma israbsorb_CFzero_CFmult :
∏ x : X, x * 0 = 0.
Show proof.

now apply ringmultx0.

Lemma isldistr_CFplus_CFmult :
∏ x y z : X, z * (x + y) = z * x + z * y.
Show proof.

now apply ringdistraxs.

Lemma isrdistr_CFplus_CFmult :
∏ x y z : X, (x + y) * z = x * z + y * z.
Show proof.

  intros.
  rewrite !(iscomm_CFmult _ z).
  now apply isldistr_CFplus_CFmult.

Lemma apCFplus :
∏ x x' y y' : X,
x + y ≠ x' + y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (apCCDRplus (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFplus_apcompat_l :
∏ x y z : X, y + x ≠ z + x <-> y ≠ z.
Show 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.

Lemma CFplus_apcompat_r :
∏ x y z : X, x + y ≠ x + z <-> y ≠ z.
Show proof.

  intros x y z.
  rewrite !(iscomm_CFplus x).
  now apply CFplus_apcompat_l.

Lemma apCFmult :
∏ x x' y y' : X,
x * y ≠ x' * y' -> x ≠ x' ∨ y ≠ y'.
Show proof.

exact (apCCDRmult (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFmult_apcompat_l :
∏ x y z : X, y * x ≠ z * x -> y ≠ z.
Show proof.

exact (CCDRmult_apcompat_l (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFmult_apcompat_l' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> y * x ≠ z * x.
Show proof.

exact (CCDRmult_apcompat_l' (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFmult_apcompat_r :
∏ x y z : X, x * y ≠ x * z -> y ≠ z.
Show proof.

exact (CCDRmult_apcompat_r (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFmult_apcompat_r' :
∏ x y z : X, x ≠ 0 -> y ≠ z -> x * y ≠ x * z.
Show proof.

exact (CCDRmult_apcompat_r' (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

Lemma CFmultapCFzero :
∏ x y : X, x * y ≠ 0 -> x ≠ 0 ∧ y ≠ 0.
Show proof.

exact (CCDRmultapCCDRzero (X := ConstructiveField_ConstructiveCommutativeDivisionRig X)).

End CF_pty.

Close Scope CF_scope.