Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.theory.fields
  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 R.

Section contents.
Context `{IsDecField F} `{forall x y: F, Decidable (x = y)}.

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

#[export] Instance decfield_zero_product : ZeroProduct F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
ZeroProduct F
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
ZeroProduct F
intros x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: x * y = 0
((x = 0) + (y = 0))%type
destruct (dec (x = 0)) as [? | Ex];auto.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: x * y = 0
Ex: x <> 0
((x = 0) + (y = 0))%type
right.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: x * y = 0
Ex: x <> 0
y = 0
rewrite <-(mult_1_r y), <-(dec_recip_inverse x) by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: x * y = 0
Ex: x <> 0
y * (x / x) = 0
rewrite associativity, (commutativity y), E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: x * y = 0
Ex: x <> 0
0 / x = 0
apply mult_0_l.
Qed.

#[export] Instance decfield_integral_domain : IsIntegralDomain F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
IsIntegralDomain F
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
IsIntegralDomain F
split; try exact _.
Qed.

Lemma dec_recip_1: / 1 = 1.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
/ 1 = 1
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
/ 1 = 1
rewrite <-(rings.mult_1_l (/1)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
1 / 1 = 1
apply dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
1 <> 0
solve_propholds.
Qed.

Lemma dec_recip_distr (x y: F): / (x * y) = / x * / y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
/ (x * y) = / x / y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
/ (x * y) = / x / y
destruct (dec (x = 0)) as [Ex|Ex].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x = 0
/ (x * y) = / x / y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
/ (x * y) = / x / y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x = 0
/ (x * y) = / x / y rewrite Ex, left_absorb, dec_recip_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x = 0
0 = 0 / y apply symmetry,mult_0_l.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
/ (x * y) = / x / y destruct (dec (y = 0)) as [Ey|Ey].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y = 0
/ (x * y) = / x / y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
/ (x * y) = / x / y
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y = 0
/ (x * y) = / x / y rewrite Ey, dec_recip_0, !mult_0_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y = 0
/ 0 = 0 exact dec_recip_0.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
/ (x * y) = / x / y assert (x * y <> 0) as Exy by (apply mult_ne_0;trivial).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
/ (x * y) = / x / y
    apply (left_cancellation_ne_0 (.*.) (x * y)); trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
(x * y) / (x * y) = x * y * (/ x / y)
    transitivity (x / x * (y / y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
(x * y) / (x * y) = x / x * (y / y)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
x / x * (y / y) = x * y * (/ x / y)
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
(x * y) / (x * y) = x / x * (y / y) rewrite !dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 = 1 * 1 rewrite mult_1_l;apply reflexivity.
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
x / x * (y / y) = x * y * (/ x / y) rewrite !dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 * 1 = x * y * (/ x / y)
      rewrite mult_assoc, (mult_comm x), <-(mult_assoc y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 * 1 = (y * (x / x)) / y
      rewrite dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 * 1 = (y * 1) / y
      rewrite (mult_comm y), <-mult_assoc.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 * 1 = 1 * (y / y)
      rewrite dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Ex: x <> 0
Ey: y <> 0
Exy: x * y <> 0
1 * 1 = 1 * 1 reflexivity.
Qed.

Lemma dec_recip_zero x : / x = 0 <-> x = 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
/ x = 0 <-> x = 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
/ x = 0 <-> x = 0
split; intros E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
x = 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: x = 0
/ x = 0
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
x = 0 apply stable.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
~~ (x = 0) intros Ex.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
Ex: x <> 0
Empty
  destruct (is_ne_0 1).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
Ex: x <> 0
1 = 0
  rewrite <-(dec_recip_inverse x), E by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: / x = 0
Ex: x <> 0
x * 0 = 0
  apply mult_0_r.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: x = 0
/ x = 0 rewrite E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E: x = 0
/ 0 = 0 exact dec_recip_0.
Qed.

Lemma dec_recip_ne_0_iff x : / x <> 0 <-> x <> 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
/ x <> 0 <-> x <> 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
/ x <> 0 <-> x <> 0
split; intros E1 E2; destruct E1; apply dec_recip_zero;trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E2: x = 0
/ / x = 0
do 2 apply (snd (dec_recip_zero _)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
E2: x = 0
x = 0 trivial.
Qed.

Instance dec_recip_ne_0 x : PropHolds (x <> 0) -> PropHolds (/x <> 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
PropHolds (x <> 0) -> PropHolds (/ x <> 0)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
PropHolds (x <> 0) -> PropHolds (/ x <> 0)
intro.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
X: PropHolds (x <> 0)
PropHolds (/ x <> 0)
apply (snd (dec_recip_ne_0_iff _)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
X: PropHolds (x <> 0)
x <> 0
trivial.
Qed.

Lemma equal_by_one_quotient (x y : F) : x / y = 1 -> x = y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
x / y = 1 -> x = y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
x / y = 1 -> x = y
intro Exy.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
x = y
destruct (dec (y = 0)) as [Ey|Ey].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y = 0
x = y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
x = y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y = 0
x = y destruct (is_ne_0 1).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y = 0
1 = 0
  rewrite <- Exy, Ey, dec_recip_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y = 0
x * 0 = 0 apply mult_0_r.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
x = y apply (right_cancellation_ne_0 (.*.) (/y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
/ y <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
x / y = y / y
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
/ y <> 0 apply dec_recip_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
PropHolds (y <> 0) trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
Exy: x / y = 1
Ey: y <> 0
x / y = y / y rewrite dec_recip_inverse;trivial.
Qed.

#[export] Instance dec_recip_inj: IsInjective (/).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
IsInjective dec_recip
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
IsInjective dec_recip
repeat (split; try exact _).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
IsInjective dec_recip
intros x y E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
x = y
destruct (dec (y = 0)) as [Ey|Ey].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y = 0
x = y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x = y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y = 0
x = y rewrite Ey in *.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / 0
Ey: y = 0
x = 0 rewrite dec_recip_0 in E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = 0
Ey: y = 0
x = 0
  apply dec_recip_zero.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = 0
Ey: y = 0
/ x = 0 trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x = y apply (right_cancellation_ne_0 (.*.) (/y)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
/ y <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x / y = y / y
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
/ y <> 0 apply dec_recip_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
PropHolds (y <> 0) trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x / y = y / y rewrite dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x / y = 1
    rewrite <-E, dec_recip_inverse;trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
x <> 0
    apply dec_recip_ne_0_iff.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
/ x <> 0 rewrite E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
/ y <> 0
    apply dec_recip_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
E: / x = / y
Ey: y <> 0
PropHolds (y <> 0) trivial.
Qed.

#[export] Instance dec_recip_involutive: Involutive (/).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
Involutive dec_recip
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
Involutive dec_recip
intros x.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
/ / x = x destruct (dec (x = 0)) as [Ex|Ex].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
/ / x = x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ / x = x
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
/ / x = x rewrite Ex, !dec_recip_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
0 = 0 trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ / x = x apply (right_cancellation_ne_0 (.*.) (/x)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ / x / x = x / x
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ x <> 0 apply dec_recip_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
PropHolds (x <> 0) trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ / x / x = x / x rewrite dec_recip_inverse by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ / x / x = 1
    rewrite mult_comm, dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
1 = 1
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ x <> 0
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
1 = 1 reflexivity.
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
/ x <> 0 apply dec_recip_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
PropHolds (x <> 0) trivial.
Qed.

Lemma equal_dec_quotients (a b c d : F) : b <> 0 -> d <> 0 ->
  (a * d = c * b <-> a / b = c / d).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
b <> 0 -> d <> 0 -> a * d = c * b <-> a / b = c / d
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
b <> 0 -> d <> 0 -> a * d = c * b <-> a / b = c / d
split; intro E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b = c / d
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d = c * b
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b = c / d apply (right_cancellation_ne_0 (.*.) b);trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b * b = c / d * b
  apply (right_cancellation_ne_0 (.*.) d);trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b * b * d = c / d * b * d
  transitivity (a * d * (b * /b));[|
  transitivity (c * b * (d * /d))].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b * b * d = a * d * (b / b)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a * d * (b / b) = c * b * (d / d)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
c * b * (d / d) = c / d * b * d
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a / b * b * d = a * d * (b / b) rewrite <-!(mult_assoc a).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a * (/ b * b * d) = a * (d * (b / b)) apply ap.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
/ b * b * d = d * (b / b)
    rewrite (mult_comm d), (mult_comm _ b).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
b / b * d = b / b * d
    reflexivity.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
a * d * (b / b) = c * b * (d / d) rewrite E, dec_recip_inverse, dec_recip_inverse;trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
c * b * (d / d) = c / d * b * d rewrite <-!(mult_assoc c).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
c * (b * (d / d)) = c * (/ d * b * d) apply ap.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
b * (d / d) = / d * b * d
    rewrite (mult_comm d), mult_assoc, (mult_comm b).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a * d = c * b
/ d * b * d = / d * b * d
    reflexivity.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d = c * b transitivity (a * d * 1);[rewrite mult_1_r;reflexivity|].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d * 1 = c * b
  rewrite <-(dec_recip_inverse b);trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d * (b / b) = c * b
  transitivity (c * b * 1);[|rewrite mult_1_r;reflexivity].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d * (b / b) = c * b * 1
  rewrite <-(dec_recip_inverse d);trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
a * d * (b / b) = c * b * (d / d)
  rewrite mult_comm, <-mult_assoc, (mult_assoc _ a), (mult_comm _ a), E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
b * (c / d * d) = c * b * (d / d)
  rewrite <-mult_assoc.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
b * (c * (/ d * d)) = c * b * (d / d) rewrite (mult_comm _ d).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
b * (c * (d / d)) = c * b * (d / d)
  rewrite mult_assoc, (mult_comm c).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, b, c, d: F
X: b <> 0
X0: d <> 0
E: a / b = c / d
b * c * (d / d) = b * c * (d / d) reflexivity.
Qed.

Lemma dec_quotients (a c b d : F)
  : b <> 0 -> d <> 0 -> a / b + c / d = (a * d + c * b) / (b * d).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
b <> 0 ->
d <> 0 -> a / b + c / d = (a * d + c * b) / (b * d)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
b <> 0 ->
d <> 0 -> a / b + c / d = (a * d + c * b) / (b * d)
intros A B.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
a / b + c / d = (a * d + c * b) / (b * d)
assert (a / b = (a * d) / (b * d)) as E1.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
a / b = (a * d) / (b * d)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
a / b + c / d = (a * d + c * b) / (b * d)
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
a / b = (a * d) / (b * d) apply equal_dec_quotients;auto.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
b * d <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
a * (b * d) = a * d * b
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
b * d <> 0 solve_propholds.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
a * (b * d) = a * d * b rewrite (mult_comm b);apply associativity.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
a / b + c / d = (a * d + c * b) / (b * d) assert (c / d = (b * c) / (b * d)) as E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
c / d = (b * c) / (b * d)
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
E2: c / d = (b * c) / (b * d)
a / b + c / d = (a * d + c * b) / (b * d)
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
c / d = (b * c) / (b * d) apply equal_dec_quotients;trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
b * d <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
c * (b * d) = b * c * d
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
b * d <> 0 solve_propholds.
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
c * (b * d) = b * c * d rewrite mult_assoc, (mult_comm c).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
b * c * d = b * c * d reflexivity.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
E2: c / d = (b * c) / (b * d)
a / b + c / d = (a * d + c * b) / (b * d) rewrite E1, E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
E2: c / d = (b * c) / (b * d)
(a * d) / (b * d) + (b * c) / (b * d) =
(a * d + c * b) / (b * d)
    rewrite (mult_comm c b).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
a, c, b, d: F
A: b <> 0
B: d <> 0
E1: a / b = (a * d) / (b * d)
E2: c / d = (b * c) / (b * d)
(a * d) / (b * d) + (b * c) / (b * d) =
(a * d + b * c) / (b * d)
    apply symmetry, simple_distribute_r.
Qed.

Lemma dec_recip_swap_l x y: x / y = / (/ x * y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
x / y = / (/ x * y)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
x / y = / (/ x * y)
rewrite dec_recip_distr, involutive.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
x / y = x / y reflexivity.
Qed.

Lemma dec_recip_swap_r x y: / x * y = / (x / y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
/ x * y = / (x / y)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
/ x * y = / (x / y)
rewrite dec_recip_distr, involutive.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x, y: F
/ x * y = / x * y
reflexivity.
Qed.

Lemma dec_recip_negate x : -(/ x) = / (-x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
- / x = / - x
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
- / x = / - x
destruct (dec (x = 0)) as [Ex|Ex].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
- / x = / - x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- / x = / - x
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
- / x = / - x rewrite Ex, negate_0, dec_recip_0, negate_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x = 0
0 = 0 reflexivity.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- / x = / - x apply (left_cancellation_ne_0 (.*.) (-x)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x * - / x = - x / - x
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x <> 0 apply (snd (flip_negate_ne_0 _)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
x <> 0 trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x * - / x = - x / - x rewrite dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x * - / x = 1
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x <> 0
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x * - / x = 1 rewrite negate_mult_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
x / x = 1 apply dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
x <> 0 trivial.
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
- x <> 0 apply (snd (flip_negate_ne_0 _)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: forall x y : F, Decidable (x = y)
x: F
Ex: x <> 0
x <> 0 trivial.
Qed.
End contents.

(* Due to bug #2528 *)
#[export]
Hint Extern 7 (PropHolds (/ _ <> 0)) =>
  eapply @dec_recip_ne_0 : typeclass_instances.

(* Given a decidable field we can easily construct a constructive field. *)
Section is_field.
  Context `{IsDecField F} `{Apart F} `{!TrivialApart F}
    `{Decidable.DecidablePaths F}.

  #[export] Instance recip_dec_field: Recip F := fun x => / x.1.

  Local Existing Instance dec_strong_setoid.

  #[export] Instance decfield_field : IsField F.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
IsField F
  Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
IsField F
  split; try exact _.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
StrongBinaryExtensionality plus
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
StrongBinaryExtensionality mult
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
forall x : {y : F & y ≶ 0}, x.1 // x = 1
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
StrongBinaryExtensionality plus exact (dec_strong_binary_morphism (+)).
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
StrongBinaryExtensionality mult exact (dec_strong_binary_morphism (.*.)).
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
forall x : {y : F & y ≶ 0}, x.1 // x = 1 intros [x Px].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: x ≶ 0
(x; Px).1 // (x; Px) = 1 rapply (dec_recip_inverse x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: x ≶ 0
x <> 0
    apply trivial_apart.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: x ≶ 0
x ≶ 0 trivial.
  Qed.

  Lemma dec_recip_correct (x : F) Px : / x = // (x;Px).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
/ x = // (x; Px)
  Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
/ x = // (x; Px)
  apply (left_cancellation_ne_0 (.*.) x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
x / x = x // (x; Px)
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
x <> 0 apply trivial_apart.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
x ≶ 0 trivial.
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
x / x = x // (x; Px) rewrite dec_recip_inverse, reciperse_alt by (apply trivial_apart;trivial).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
H1: DecidablePaths F
x: F
Px: (fun y : F => y ≶ 0) x
1 = 1
    reflexivity.
  Qed.
End is_field.

(* Definition stdlib_field_theory F `{DecField F} :
  Field_theory.field_theory 0 1 (+) (.*.) (fun x y => x - y)
    (-) (fun x y => x / y) (/) (=).
Proof with auto.
  intros.
  constructor.
     apply (theory.rings.stdlib_ring_theory _).
    apply (is_ne_0 1).
   reflexivity.
  intros.
  rewrite commutativity. by apply dec_recip_inverse.
Qed. *)

(* Section from_stdlib_field_theory.
  Context `(ftheory : @field_theory F Fzero Fone Fplus Fmult Fminus Fnegate
    Fdiv Frecip Fe)
    (rinv_0 : Fe (Frecip Fzero) Fzero)
    `{!@Setoid F Fe}
    `{!Proper (Fe ==> Fe ==> Fe) Fplus}
    `{!Proper (Fe ==> Fe ==> Fe) Fmult}
    `{!Proper (Fe ==> Fe) Fnegate}
    `{!Proper (Fe ==> Fe) Frecip}.

  Add Field F2 : ftheory.

  Definition from_stdlib_field_theory: @DecField F Fe Fplus Fmult
    Fzero Fone Fnegate Frecip.
  Proof with auto.
   destruct ftheory.
   repeat (constructor; try assumption); repeat intro
   ; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
     one_is_mon_unit, mult_is_sg_op, plus, mult, recip, negate; try field.
   unfold recip, mult.
   simpl.
   assert (Fe (Fmult x (Frecip x)) (Fmult (Frecip x) x)) as E by ring.
   rewrite E.
  Qed.
End from_stdlib_field_theory. *)

Section morphisms.
  Context  `{IsDecField F} `{TrivialApart F} `{Decidable.DecidablePaths F}.

  #[export] Instance dec_field_to_domain_inj `{IsIntegralDomain R}
    `{!IsSemiRingPreserving (f : F -> R)} : IsInjective f.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
IsInjective f
  Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
IsInjective f
  apply injective_preserves_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
forall x : F, f x = 0 -> x = 0
  intros x Efx.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
x = 0
  apply stable.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
~~ (x = 0) intros Ex.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
Ex: x <> 0
Empty
  destruct (is_ne_0 (1:R)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
Ex: x <> 0
1 = 0
  rewrite <-(rings.preserves_1 (f:=f)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
Ex: x <> 0
f 1 = 0
  rewrite <-(dec_recip_inverse x) by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
Ex: x <> 0
f (x / x) = 0
  rewrite rings.preserves_mult, Efx.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
R: Type
Aplus0: Plus R
Amult0: Mult R
Azero0: Zero R
Aone0: One R
Anegate0: Negate R
H2: IsIntegralDomain R
f: F -> R
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> R)
x: F
Efx: f x = 0
Ex: x <> 0
0 * f (/ x) = 0
  apply left_absorb.
  Qed.

  Lemma preserves_dec_recip `{IsDecField F2} `{forall x y: F2, Decidable (x = y)}
    `{!IsSemiRingPreserving (f : F -> F2)} x : f (/ x) = / f x.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
f (/ x) = / f x
  Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
f (/ x) = / f x
  case (dec (x = 0)) as [E | E].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x = 0
f (/ x) = / f x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f (/ x) = / f x
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x = 0
f (/ x) = / f x rewrite E, dec_recip_0, preserves_0, dec_recip_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x = 0
0 = 0 reflexivity.
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f (/ x) = / f x intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f (/ x) = / f x
    apply (left_cancellation_ne_0 (.*.) (f x)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x * f (/ x) = f x / f x
    +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x <> 0 apply isinjective_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
PropHolds (x <> 0) trivial.
    +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x * f (/ x) = f x / f x rewrite <-preserves_mult, 2!dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f 1 = 1
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
x <> 0
      *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f 1 = 1 exact preserves_1.
      *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
f x <> 0 apply isinjective_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
PropHolds (x <> 0) trivial.
      *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Adec_recip0: DecRecip F2
H2: IsDecField F2
H3: forall x y : F2, Decidable (x = y)
f: F -> F2
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : F -> F2)
x: F
E: x <> 0
x <> 0 trivial.
  Qed.

  Lemma dec_recip_to_recip `{IsField F2} `{!IsSemiRingStrongPreserving (f : F -> F2)}
    x Pfx : f (/ x) = // (f x;Pfx).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
f (/ x) = // (f x; Pfx)
  Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
f (/ x) = // (f x; Pfx)
  assert (x <> 0).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f (/ x) = // (f x; Pfx)
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
x <> 0 intros Ex.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
Ex: x = 0
Empty
    destruct (apart_ne (f x) 0 Pfx).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
Ex: x = 0
f x = 0
    rewrite Ex, (preserves_0 (f:=f)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
Ex: x = 0
0 = 0 reflexivity.
  -
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f (/ x) = // (f x; Pfx) apply (left_cancellation_ne_0 (.*.) (f x)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f x <> 0
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f x * f (/ x) = f x // (f x; Pfx)
    +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f x <> 0 apply isinjective_ne_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
PropHolds (x <> 0) trivial.
    +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f x * f (/ x) = f x // (f x; Pfx) rewrite <-preserves_mult, dec_recip_inverse, reciperse_alt by assumption.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
Aap: Apart F
H0: TrivialApart F
H1: DecidablePaths F
F2: Type
Aplus0: Plus F2
Amult0: Mult F2
Azero0: Zero F2
Aone0: One F2
Anegate0: Negate F2
Aap0: Apart F2
Arecip: Recip F2
H2: IsField F2
f: F -> F2
IsSemiRingStrongPreserving0: IsSemiRingStrongPreserving
  (f : F -> F2)
x: F
Pfx: (fun y : F2 => y ≶ 0) (f x)
X: x <> 0
f 1 = 1
      exact preserves_1.
  Qed.
End morphisms.