Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.theory.apartness.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export
  HoTT.Classes.theory.rings.

Generalizable Variables F f.

Section field_properties.
Context `{IsField F}.

Definition recip' (x : F) (apx : x ≶ 0) : F := //(x;apx).

(* Add Ring F : (stdlib_ring_theory F). *)
Lemma recip_inverse' (x : F) (Px : x ≶ 0) : x // (x; Px) = 1.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x // (x; Px) = 1
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x // (x; Px) = 1
  apply (recip_inverse (x;Px)).
Qed.

Lemma reciperse_alt (x : F) Px : x // (x;Px) = 1.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: (fun y : F => y ≶ 0) x
x // (x; Px) = 1
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: (fun y : F => y ≶ 0) x
x // (x; Px) = 1
rewrite <-(recip_inverse (x;Px)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: (fun y : F => y ≶ 0) x
x // (x; Px) = (x; Px).1 // (x; Px) trivial.
Qed.

Lemma recip_proper_alt x y Px Py : x = y -> // (x;Px) = // (y;Py).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
x = y -> // (x; Px) = // (y; Py)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
x = y -> // (x; Px) = // (y; Py)
intro E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
E: x = y
// (x; Px) = // (y; Py) apply ap.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
E: x = y
(x; Px) = (y; Py)
apply Sigma.path_sigma with E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
E: x = y
transport (fun y : F => y ≶ 0) E (x; Px).2 = (y; Py).2
apply path_ishprop.
Qed.

Lemma recip_proper x y Py : x // (y;Py) = 1 -> x = y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
x // (y; Py) = 1 -> x = y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
x // (y; Py) = 1 -> x = y
  intros eqxy.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = y
  rewrite <- (mult_1_r y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = y * 1
  rewrite <- eqxy.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = y * (x // (y; Py))
  rewrite (mult_assoc y x (//(y;Py))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = y * x // (y; Py)
  rewrite (mult_comm y x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = x * y // (y; Py)
  rewrite <- (mult_assoc x y (//(y;Py))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = x * (y // (y; Py))
  rewrite (recip_inverse (y;Py)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = x * 1
  rewrite (mult_1_r x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Py: (fun y : F => y ≶ 0) y
eqxy: x // (y; Py) = 1
x = x
  reflexivity.
Qed.

Lemma recip_irrelevant x Px1 Px2 : // (x;Px1) = // (x;Px2).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px1, Px2: (fun y : F => y ≶ 0) x
// (x; Px1) = // (x; Px2)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px1, Px2: (fun y : F => y ≶ 0) x
// (x; Px1) = // (x; Px2)
apply recip_proper_alt.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px1, Px2: (fun y : F => y ≶ 0) x
x = x reflexivity.
Qed.

Lemma apart_0_proper {x y} : x ≶ 0 -> x = y -> y ≶ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x ≶ 0 -> x = y -> y ≶ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x ≶ 0 -> x = y -> y ≶ 0
intros ? E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x ≶ 0
E: x = y
y ≶ 0 rewrite <-E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x ≶ 0
E: x = y
x ≶ 0 trivial.
Qed.

Global Instance: IsStrongInjective (-).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
IsStrongInjective negate
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
IsStrongInjective negate
repeat (split; try apply _); intros x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: x ≶ y
- x ≶ - y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: - x ≶ - y
x ≶ y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: x ≶ y
- x ≶ - y apply (strong_extensionality (+ x + y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: x ≶ y
- x + (x + y) ≶ - y + (x + y)
  rewrite simple_associativity, left_inverse, plus_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: x ≶ y
y ≶ - y + (x + y)
  rewrite (commutativity (f:=plus) x y), simple_associativity,
    left_inverse, plus_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: x ≶ y
y ≶ x
  apply symmetry;trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: - x ≶ - y
x ≶ y apply (strong_extensionality (+ -x + -y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: - x ≶ - y
x + (- x - y) ≶ y + (- x - y)
  rewrite simple_associativity, right_inverse, plus_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: - x ≶ - y
- y ≶ y + (- x - y)
  rewrite (commutativity (f:=plus) (- x) (- y)),
    simple_associativity, right_inverse, plus_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
E: - x ≶ - y
- y ≶ - x
  apply symmetry;trivial.
Qed.

Global Instance: IsStrongInjective (//).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
IsStrongInjective recip
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
IsStrongInjective recip
repeat (split; try apply _); intros x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
// x ≶ // y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
x ≶ y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
// x ≶ // y apply (strong_extensionality (x.1 *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
x.1 // x ≶ x.1 // y
  rewrite recip_inverse, (commutativity (f:=mult)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
1 ≶ // y * x.1
  apply (strong_extensionality (y.1 *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
y.1 * 1 ≶ y.1 * (// y * x.1)
  rewrite simple_associativity, recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
y.1 * 1 ≶ 1 * x.1
  rewrite mult_1_l,mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: x ≶ y
y.1 ≶ x.1 apply symmetry;trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
x ≶ y apply (strong_extensionality (.* // x)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
x.1 // x ≶ y.1 // x
  rewrite recip_inverse, (commutativity (f:=mult)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
1 ≶ // x * y.1
  apply (strong_extensionality (.* // y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
1 // y ≶ // x * y.1 // y
  rewrite <-simple_associativity, recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
1 // y ≶ // x * 1
  rewrite mult_1_l,mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: ApartZero F
E: // x ≶ // y
// y ≶ // x apply symmetry;trivial.
Qed.

Global Instance: forall z, StrongLeftCancellation (+) z.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F, StrongLeftCancellation plus z
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F, StrongLeftCancellation plus z
intros z x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z, x, y: F
E: x ≶ y
z + x ≶ z + y apply (strong_extensionality (+ -z)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z, x, y: F
E: x ≶ y
z + x - z ≶ z + y - z
do 2 rewrite (commutativity (f:=plus) z _),
  <-simple_associativity,right_inverse,plus_0_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z, x, y: F
E: x ≶ y
x ≶ y
trivial.
Qed.

Global Instance: forall z, StrongRightCancellation (+) z.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F, StrongRightCancellation plus z
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F, StrongRightCancellation plus z
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
StrongRightCancellation plus z apply (strong_right_cancel_from_left (+)).
Qed.

Global Instance: forall z, PropHolds (z ≶ 0) -> StrongLeftCancellation (.*.) z.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F,
PropHolds (z ≶ 0) -> StrongLeftCancellation mult z
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F,
PropHolds (z ≶ 0) -> StrongLeftCancellation mult z
intros z Ez x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
Ez: PropHolds (z ≶ 0)
x, y: F
E: x ≶ y
z * x ≶ z * y red in Ez.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
Ez: z ≶ 0
x, y: F
E: x ≶ y
z * x ≶ z * y
rewrite !(commutativity z).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
Ez: z ≶ 0
x, y: F
E: x ≶ y
x * z ≶ y * z
apply (strong_extensionality (.* // (z;(Ez : (≶0) z)))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
Ez: z ≶ 0
x, y: F
E: x ≶ y
x * z // (z; Ez) ≶ y * z // (z; Ez)
rewrite <-!simple_associativity, !reciperse_alt.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
Ez: z ≶ 0
x, y: F
E: x ≶ y
x * 1 ≶ y * 1
rewrite !mult_1_r;trivial.
Qed.

Global Instance: forall z, PropHolds (z ≶ 0) -> StrongRightCancellation (.*.) z.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F,
PropHolds (z ≶ 0) -> StrongRightCancellation mult z
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall z : F,
PropHolds (z ≶ 0) -> StrongRightCancellation mult z
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
z: F
X: PropHolds (z ≶ 0)
StrongRightCancellation mult z apply (strong_right_cancel_from_left (.*.)).
Qed.

Lemma mult_apart_zero_l x y : x * y ≶ 0 -> x ≶ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x * y ≶ 0 -> x ≶ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x * y ≶ 0 -> x ≶ 0
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
x ≶ 0 apply (strong_extensionality (.* y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
x * y ≶ 0 * y
rewrite mult_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
x * y ≶ 0 trivial.
Qed.

Lemma mult_apart_zero_r x y : x * y ≶ 0 -> y ≶ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x * y ≶ 0 -> y ≶ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
x * y ≶ 0 -> y ≶ 0
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
y ≶ 0 apply (strong_extensionality (x *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
x * y ≶ x * 0
rewrite mult_0_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
X: x * y ≶ 0
x * y ≶ 0 trivial.
Qed.

Instance mult_apart_zero x y :
  PropHolds (x ≶ 0) -> PropHolds (y ≶ 0) -> PropHolds (x * y ≶ 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
PropHolds (x ≶ 0) ->
PropHolds (y ≶ 0) -> PropHolds (x * y ≶ 0)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
PropHolds (x ≶ 0) ->
PropHolds (y ≶ 0) -> PropHolds (x * y ≶ 0)
intros Ex Ey.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Ex: PropHolds (x ≶ 0)
Ey: PropHolds (y ≶ 0)
PropHolds (x * y ≶ 0)
apply (strong_extensionality (.* // (y;(Ey : (≶0) y)))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Ex: PropHolds (x ≶ 0)
Ey: PropHolds (y ≶ 0)
x * y // (y; Ey) ≶ 0 // (y; Ey)
rewrite <-simple_associativity, reciperse_alt, mult_1_r, mult_0_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Ex: PropHolds (x ≶ 0)
Ey: PropHolds (y ≶ 0)
x ≶ 0
trivial.
Qed.

Instance: NoZeroDivisors F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
NoZeroDivisors F
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
NoZeroDivisors F
intros x [x_nonzero [y [y_nonzero E]]].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Empty
assert (~ ~ apart y 0) as Ey.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
~~ (y ≶ 0)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
Empty
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
~~ (y ≶ 0) intros E';apply y_nonzero,tight_apart,E'.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
Empty apply Ey.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
~ (y ≶ 0) intro y_apartzero.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
y_apartzero: y ≶ 0
Empty
  apply x_nonzero.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
y_apartzero: y ≶ 0
x = 0
  rewrite <- (mult_1_r x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
y_apartzero: y ≶ 0
x * 1 = 0 rewrite <- (reciperse_alt y y_apartzero).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
y_apartzero: y ≶ 0
x * (y // (y; y_apartzero)) = 0
  rewrite simple_associativity, E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
x_nonzero: x <> 0
y: F
y_nonzero: y <> 0
E: x * y = 0
Ey: ~~ (y ≶ 0)
y_apartzero: y ≶ 0
0 // (y; y_apartzero) = 0
  apply mult_0_l.
Qed.

Global Instance : IsIntegralDomain F := {}.

Global Instance apart_0_sig_apart_0: forall (x : ApartZero F), PropHolds (x.1 ≶ 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall x : ApartZero F, PropHolds (x.1 ≶ 0)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
forall x : ApartZero F, PropHolds (x.1 ≶ 0)
intros [??];trivial.
Qed.

Instance recip_apart_zero x : PropHolds (// x ≶ 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
PropHolds (// x ≶ 0)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
PropHolds (// x ≶ 0)
red.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
// x ≶ 0
apply mult_apart_zero_r with (x.1).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
x.1 // x ≶ 0
rewrite recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
1 ≶ 0 solve_propholds.
Qed.

Lemma field_div_0_l x y : x = 0 -> x // y = 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: ApartZero F
x = 0 -> x // y = 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: ApartZero F
x = 0 -> x // y = 0
intros E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: ApartZero F
E: x = 0
x // y = 0 rewrite E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: ApartZero F
E: x = 0
0 // y = 0 apply left_absorb.
Qed.

Lemma field_div_diag x y : x = y.1 -> x // y = 1.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: {y : F & y ≶ 0}
x = y.1 -> x // y = 1
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: {y : F & y ≶ 0}
x = y.1 -> x // y = 1
intros E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: {y : F & y ≶ 0}
E: x = y.1
x // y = 1 rewrite E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
y: {y : F & y ≶ 0}
E: x = y.1
y.1 // y = 1 apply recip_inverse.
Qed.

Lemma equal_quotients (a c: F) b d : a * d.1 = c * b.1 <-> a // b = c // d.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
a * d.1 = c * b.1 <-> a // b = c // d
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
a * d.1 = c * b.1 <-> a // b = c // d
split; intro E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a * d.1 = c * b.1
a // b = c // d
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a // b = c // d
a * d.1 = c * b.1
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a * d.1 = c * b.1
a // b = c // d rewrite <-(mult_1_l (a // b)),
  <- (recip_inverse d),
  (commutativity (f:=mult) d.1 (// d)),
  <-simple_associativity,
  (simple_associativity d.1),
  (commutativity (f:=mult) d.1 a),
  E,
  <-simple_associativity,
  simple_associativity,
  recip_inverse,
  mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a * d.1 = c * b.1
// d * c = c // d
  apply commutativity.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a // b = c // d
a * d.1 = c * b.1 rewrite <-(mult_1_r (a * d.1)),
  <- (recip_inverse b),
  <-simple_associativity,
  (commutativity (f:=mult) b.1 (// b)),
  (simple_associativity d.1),
  (commutativity (f:=mult) d.1),
  !simple_associativity,
  E,
  <-(simple_associativity c),
  (commutativity (f:=mult) (// d)),
  recip_inverse,
  mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
a, c: F
b, d: {y : F & y ≶ 0}
E: a // b = c // d
c * b.1 = c * b.1
  reflexivity.
Qed.

Lemma recip_distr_alt (x y : F) Px Py Pxy :
  // (x * y ; Pxy) = // (x;Px) * // (y;Py).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
// (x * y; Pxy) = // (x; Px) // (y; Py)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
// (x * y; Pxy) = // (x; Px) // (y; Py)
apply (left_cancellation_ne_0 (.*.) (x * y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y // (x * y; Pxy) =
x * y * (// (x; Px) // (y; Py))
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y <> 0 apply apart_ne;trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y // (x * y; Pxy) =
x * y * (// (x; Px) // (y; Py)) transitivity ((x // (x;Px)) *  (y // (y;Py))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y // (x * y; Pxy) = x // (x; Px) * (y // (y; Py))
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x // (x; Px) * (y // (y; Py)) =
x * y * (// (x; Px) // (y; Py))
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * y // (x * y; Pxy) = x // (x; Px) * (y // (y; Py)) rewrite 3!reciperse_alt,mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
1 = 1 reflexivity.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x // (x; Px) * (y // (y; Py)) =
x * y * (// (x; Px) // (y; Py)) rewrite <-simple_associativity,<-simple_associativity.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
x * (// (x; Px) * (y // (y; Py))) =
x * (y * (// (x; Px) // (y; Py)))
    apply ap.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
// (x; Px) * (y // (y; Py)) =
y * (// (x; Px) // (y; Py))
    rewrite simple_associativity.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
// (x; Px) * y // (y; Py) =
y * (// (x; Px) // (y; Py))
    rewrite (commutativity (f:=mult) _ y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
y // (x; Px) // (y; Py) = y * (// (x; Px) // (y; Py))
    rewrite <-simple_associativity.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x, y: F
Px: (fun y : F => y ≶ 0) x
Py: (fun y : F => y ≶ 0) y
Pxy: (fun y : F => y ≶ 0) (x * y)
y * (// (x; Px) // (y; Py)) =
y * (// (x; Px) // (y; Py))
    reflexivity.
Qed.

Lemma apart_negate (x : F) (Px : x ≶ 0) : (-x) ≶ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- x ≶ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- x ≶ 0
  (* Have: x <> 0 *)
  (* Want to show: -x <> 0 *)
  (* Since x=x+0 <> 0=x-x, have x<>x or 0<>-x *)
  assert (ap : x + 0 ≶ x - x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x + 0 ≶ x - x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
- x ≶ 0
  {
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x + 0 ≶ x - x
    rewrite (plus_0_r x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x ≶ x - x
    rewrite (plus_negate_r x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x ≶ 0
    assumption.
  }
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
- x ≶ 0
  refine (Trunc_rec _ (field_plus_ext F x 0 x (-x) ap)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
(x ≶ x) + (0 ≶ - x) -> - x ≶ 0
  intros [apxx|ap0x].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
apxx: x ≶ x
- x ≶ 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
ap0x: 0 ≶ - x
- x ≶ 0
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
apxx: x ≶ x
- x ≶ 0 destruct (apart_ne x x apxx); reflexivity.
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ap: x + 0 ≶ x - x
ap0x: 0 ≶ - x
- x ≶ 0 symmetry; assumption.
Qed.
Definition negate_apart : ApartZero F -> ApartZero F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
ApartZero F -> ApartZero F
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
ApartZero F -> ApartZero F
  intros [x Px].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
ApartZero F
  exists (-x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- x ≶ 0
  exact ((apart_negate x Px)).
Defined.
Lemma recip_negate (x : F) (Px : x ≶ 0) : (-//(x;Px))=//(negate_apart(x;Px)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- (// (x; Px)) = // negate_apart (x; Px)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- (// (x; Px)) = // negate_apart (x; Px)
  apply (left_cancellation (.*.) x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x * - (// (x; Px)) = x // negate_apart (x; Px)
  rewrite <- negate_mult_distr_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- (x // (x; Px)) = x // negate_apart (x; Px)
  rewrite reciperse_alt.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
-1 = x // negate_apart (x; Px)
  apply flip_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
1 = - (x // negate_apart (x; Px))
  rewrite negate_mult_distr_l.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
1 = - x // negate_apart (x; Px)
  refine (_^).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
- x // negate_apart (x; Px) = 1
  apply reciperse_alt.
Qed.
Lemma recip_apart (x : F) (Px : x ≶ 0) : // (x;Px) ≶ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
// (x; Px) ≶ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
// (x; Px) ≶ 0
  apply (strong_extensionality (x*.) (// (x; Px)) 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
x // (x; Px) ≶ x * 0
  rewrite (recip_inverse (x;Px)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
1 ≶ x * 0
  rewrite mult_0_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
Px: x ≶ 0
1 ≶ 0
  solve_propholds.
Qed.
Definition recip_on_apart (x : ApartZero F) : ApartZero F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
ApartZero F
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
ApartZero F
  exists (//x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: ApartZero F
// x ≶ 0
  apply recip_apart.
Defined.
Global Instance recip_involutive: Involutive recip_on_apart.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
Involutive recip_on_apart
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
Involutive recip_on_apart
  intros [x apx0].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
recip_on_apart (recip_on_apart (x; apx0)) = (x; apx0)
  apply path_sigma_hprop.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
(recip_on_apart (recip_on_apart (x; apx0))).1 =
(x; apx0).1
  unfold recip_on_apart.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
(//
 (// (x; apx0); recip_apart (x; apx0).1 (x; apx0).2);
recip_apart
  (// (x; apx0); recip_apart (x; apx0).1 (x; apx0).2).1
  (// (x; apx0); recip_apart (x; apx0).1 (x; apx0).2).2).1 =
(x; apx0).1
  cbn.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
// (// (x; apx0); recip_apart x apx0) = x
  apply (left_cancellation (.*.) (// (x; apx0))).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
// (x; apx0) // (// (x; apx0); recip_apart x apx0) =
// (x; apx0) * x
  rewrite (recip_inverse' (// (x; apx0)) (recip_apart x apx0)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
1 = // (x; apx0) * x
  rewrite mult_comm.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
1 = x // (x; apx0)
  rewrite (recip_inverse (x;apx0)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Aap: Apart F
Arecip: Recip F
H: IsField F
x: F
apx0: x ≶ 0
1 = 1
  reflexivity.
Qed.

End field_properties.

(* Due to bug #2528 *)
#[export]
Hint Extern 8 (PropHolds (// _ ≶ 0)) =>
  eapply @recip_apart_zero : typeclass_instances.
#[export]
Hint Extern 8 (PropHolds (_ * _ ≶ 0)) =>
  eapply @mult_apart_zero : typeclass_instances.

Section morphisms.
  Context `{IsField F1} `{IsField F2} `{!IsSemiRingStrongPreserving (f : F1 -> F2)}.

(*   Add Ring F1 : (stdlib_ring_theory F1). *)

  Lemma strong_injective_preserves_0 : (forall x, x ≶ 0 -> f x ≶ 0) -> IsStrongInjective f.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
(forall x : F1, x ≶ 0 -> f x ≶ 0) ->
IsStrongInjective f
  Proof.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
(forall x : F1, x ≶ 0 -> f x ≶ 0) ->
IsStrongInjective f
  intros E1.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
IsStrongInjective f split; try apply _.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
forall x y : F1, x ≶ y -> f x ≶ f y intros x y E2.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
f x ≶ f y
  apply (strong_extensionality (+ -f y)).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
f x - f y ≶ f y - f y
  rewrite plus_negate_r, <-preserves_minus.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
f (x - y) ≶ 0
  apply E1.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
x - y ≶ 0
  apply (strong_extensionality (+ y)).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
x - y + y ≶ 0 + y
  rewrite <-simple_associativity,left_inverse,plus_0_l,plus_0_r.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
E1: forall x : F1, x ≶ 0 -> f x ≶ 0
x, y: F1
E2: x ≶ y
x ≶ y
  trivial.
  Qed.

  (* We have the following for morphisms to non-trivial strong rings as well.
    However, since we do not have an interface for strong rings, we ignore it. *)
  Global Instance: IsStrongInjective f.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
IsStrongInjective f
  Proof.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
IsStrongInjective f
  apply strong_injective_preserves_0.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
forall x : F1, x ≶ 0 -> f x ≶ 0
  intros x Ex.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Ex: x ≶ 0
f x ≶ 0
  apply mult_apart_zero_l with (f (// exist (≶0) x Ex)).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Ex: x ≶ 0
f x * f (// (x; Ex)) ≶ 0
  rewrite <-rings.preserves_mult.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Ex: x ≶ 0
f (x // (x; Ex)) ≶ 0
  rewrite reciperse_alt.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Ex: x ≶ 0
f 1 ≶ 0
  rewrite (rings.preserves_1 (f:=f)).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Ex: x ≶ 0
1 ≶ 0
  solve_propholds.
  Qed.

  Lemma preserves_recip x Px Pfx : f (// (x;Px)) = // (f x;Pfx).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f (// (x; Px)) = // (f x; Pfx)
  Proof.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f (// (x; Px)) = // (f x; Pfx)
  apply (left_cancellation_ne_0 (.*.) (f x)).
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f x <> 0
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f x * f (// (x; Px)) = f x // (f x; Pfx)
  -
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f x <> 0 apply apart_ne;trivial.
  -
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f x * f (// (x; Px)) = f x // (f x; Pfx) rewrite <-rings.preserves_mult.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f (x // (x; Px)) = f x // (f x; Pfx)
    rewrite !reciperse_alt.
F1: Type
Aplus: Plus F1
Amult: Mult F1
Azero: Zero F1
Aone: One F1
Anegate: Negate F1
Aap: Apart F1
Arecip: Recip F1
H: IsField F1
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip0: Recip F2
H0: IsField F2
f: F1 -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F1 -> F2)
x: F1
Px: (fun y : F1 => y ≶ 0) x
Pfx: (fun y : F2 => y ≶ 0) (f x)
f 1 = 1
    apply preserves_1.
  Qed.
End morphisms.