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

Generalizable Variables F f R Fle Flt.

Section contents.
Context `{OrderedField F}.

Lemma pos_recip_compat (x : F) (Px : 0 < x) : 0 < //(x;positive_apart_zero x Px).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: 0 < x
0 < // (x; positive_apart_zero x Px)
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: 0 < x
0 < // (x; positive_apart_zero x Px)
apply (strictly_order_reflecting (x *.)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: 0 < x
x * 0 < x // (x; positive_apart_zero x Px)
rewrite mult_0_r.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: 0 < x
0 < x // (x; positive_apart_zero x Px)
rewrite (recip_inverse' x).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: 0 < x
0 < 1
exact lt_0_1.
Qed.

Lemma neg_recip_compat (x : F) (Px : x < 0) : //(x;negative_apart_zero x Px) < 0.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
// (x; negative_apart_zero x Px) < 0
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
// (x; negative_apart_zero x Px) < 0
  set (negxpos := fst (flip_neg_negate x) Px).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
negxpos:= fst (flip_neg_negate x) Px: 0 < - x
// (x; negative_apart_zero x Px) < 0
  apply (strictly_order_reflecting ((-x) *.)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
negxpos:= fst (flip_neg_negate x) Px: 0 < - x
- x // (x; negative_apart_zero x Px) < - x * 0
  rewrite mult_0_r.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
negxpos:= fst (flip_neg_negate x) Px: 0 < - x
- x // (x; negative_apart_zero x Px) < 0
  rewrite <- negate_mult_distr_l.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
negxpos:= fst (flip_neg_negate x) Px: 0 < - x
- (x // (x; negative_apart_zero x Px)) < 0
  rewrite (recip_inverse' x).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
Px: x < 0
negxpos:= fst (flip_neg_negate x) Px: 0 < - x
-1 < 0
  apply flip_pos_negate, lt_0_1.
Qed.

Lemma flip_lt_recip x y (Py : 0 < y) (ltyx : y < x) :
  let apy0 := positive_apart_zero y Py in
  let apx0 := positive_apart_zero x (transitivity Py ltyx) in
  //(x;apx0) < //(y;apy0).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
let apy0 := positive_apart_zero y Py in
let apx0 :=
  positive_apart_zero x (transitivity Py ltyx) in
// (x; apx0) < // (y; apy0)
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
let apy0 := positive_apart_zero y Py in
let apx0 :=
  positive_apart_zero x (transitivity Py ltyx) in
// (x; apx0) < // (y; apy0)
  assert (0 < x) by (transitivity y;trivial).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
let apy0 := positive_apart_zero y Py in
let apx0 :=
  positive_apart_zero x (transitivity Py ltyx) in
// (x; apx0) < // (y; apy0)
  apply (strictly_order_reflecting (x *.)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
x // (x; positive_apart_zero x (transitivity Py ltyx)) <
x // (y; positive_apart_zero y Py)
  rewrite (recip_inverse' x ).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
1 < x // (y; positive_apart_zero y Py)
  rewrite mult_comm.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
1 < // (y; positive_apart_zero y Py) * x
  apply (strictly_order_reflecting (y *.)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
y * 1 < y * (// (y; positive_apart_zero y Py) * x)
  rewrite mult_assoc, mult_1_r.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: y < x
X: 0 < x
y < y // (y; positive_apart_zero y Py) * x
  rewrite (recip_inverse' y), mult_1_l; assumption.
Qed.

Lemma flip_lt_recip_l x y (Py : 0 < y) (ltyx : //(y;positive_apart_zero y Py) < x) :
  let apx0 := positive_apart_zero x (transitivity (pos_recip_compat y Py) ltyx) in
  //(x;apx0) < y.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
  set (apy0 := positive_apart_zero y Py).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
  set (eq := recip_involutive (y;apy0)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
  set (eq' := ap pr1 eq).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: (recip_on_apart (recip_on_apart (y; apy0))).1 =
(y; apy0).1
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
  cbn in eq'.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
let apx0 :=
  positive_apart_zero x
    (transitivity (pos_recip_compat y Py) ltyx) in
// (x; apx0) < y
  rewrite <- eq'.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// recip_on_apart (y; apy0)
  unfold recip_on_apart.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  (* need : // (y; apy0) < x *)
  (* have : //(y;pseudo_order_lt_apart_flip 0 y Py) < x *)
  set (ltyx2 := ltyx).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2:= ltyx: // (y; positive_apart_zero y Py) < x
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx2)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  unfold ltyx2.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2:= ltyx: // (y; positive_apart_zero y Py) < x
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  rewrite (recip_irrelevant y (positive_apart_zero y Py) apy0) in ltyx2.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  set (ltyx_recips := flip_lt_recip x (// (y; apy0)) (pos_recip_compat y Py) ltyx2).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
ltyx_recips:= flip_lt_recip x (// (y; apy0))
  (pos_recip_compat y Py) ltyx2: let apy1 :=
  positive_apart_zero (// (y; apy0))
    (pos_recip_compat y Py) in
let apx0 :=
  positive_apart_zero x
    (transitivity
       (pos_recip_compat y Py) ltyx2) in
// (x; apx0) < // (// (y; apy0); apy1)
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  cbn in ltyx_recips.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
ltyx_recips:= flip_lt_recip x (// (y; apy0))
  (pos_recip_compat y Py) ltyx2: //
(x;
positive_apart_zero x
  (strictorder_trans 0 (// (y; apy0)) x
     (pos_recip_compat y Py) ltyx2)) <
//
(// (y; apy0);
positive_apart_zero (// (y; apy0))
  (pos_recip_compat y Py))
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  rewrite (recip_irrelevant x _ (positive_apart_zero x (transitivity (pos_recip_compat y Py) ltyx))) in ltyx_recips.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
ltyx_recips: //
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py)
     ltyx)) <
//
(// (y; apy0);
positive_apart_zero (// (y; apy0))
  (pos_recip_compat y Py))
//
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart (y; apy0).1 (y; apy0).2)
  cbn.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
ltyx_recips: //
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py)
     ltyx)) <
//
(// (y; apy0);
positive_apart_zero (// (y; apy0))
  (pos_recip_compat y Py))
//
(x;
positive_apart_zero x
  (strictorder_trans 0 (// (y; apy0)) x
     (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart y apy0)
  rewrite (recip_irrelevant (//(y;apy0)) _ (recip_apart y apy0)) in ltyx_recips.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Py: 0 < y
ltyx: // (y; positive_apart_zero y Py) < x
apy0:= positive_apart_zero y Py: y ≶ 0
eq:= recip_involutive (y; apy0): recip_on_apart (recip_on_apart (y; apy0)) =
(y; apy0)
eq':= ap pr1 eq: // recip_on_apart (y; apy0) = y
ltyx2: // (y; apy0) < x
ltyx_recips: //
(x;
positive_apart_zero x
  (transitivity (pos_recip_compat y Py)
     ltyx)) <
// (// (y; apy0); recip_apart y apy0)
//
(x;
positive_apart_zero x
  (strictorder_trans 0 (// (y; apy0)) x
     (pos_recip_compat y Py) ltyx)) <
// (// (y; apy0); recip_apart y apy0)
  assumption.
Qed.
Lemma flip_lt_recip_r (x y : F) (Px : 0 < x) (Py : 0 < y) (ltyx : y < //(x;positive_apart_zero x Px)) :
  x < //(y;positive_apart_zero y Py).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
x < // (y; positive_apart_zero y Py)
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
x < // (y; positive_apart_zero y Py)
  set (apx0 := positive_apart_zero x Px).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
x < // (y; positive_apart_zero y Py)
  set (apy0 := positive_apart_zero y Py).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
x < // (y; apy0)
  change x with ((x;apx0) : ApartZero F).1.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
((x; apx0) : ApartZero F).1 < // (y; apy0)
  rewrite <- (recip_involutive (x;apx0)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
(recip_on_apart (recip_on_apart (x; apx0))).1 <
// (y; apy0)
  unfold recip_on_apart; cbn.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  assert (ltry := pos_recip_compat y Py).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; positive_apart_zero y Py)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  rewrite (recip_irrelevant y (positive_apart_zero y Py) apy0) in ltry.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
ltyx: y < // (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  change y with ((y;apy0) : ApartZero F).1 in ltyx.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltyx: ((y; apy0) : ApartZero F).1 <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltry: 0 < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  rewrite <- (recip_involutive (y;apy0)) in ltyx.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltyx: (recip_on_apart (recip_on_apart (y; apy0))).1 <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltry: 0 < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  unfold recip_on_apart in ltyx; cbn in ltyx.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltyx: // (// (y; apy0); recip_apart y apy0) <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltry: 0 < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  rewrite (recip_irrelevant (//(y;apy0)) (recip_apart y apy0) (positive_apart_zero (// (y; apy0)) ltry)) in ltyx.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; apy0)
ltyx: //
(// (y; apy0);
positive_apart_zero (// (y; apy0)) ltry) <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  assert (ltxy := flip_lt_recip_l (// (x; apx0)) (// (y; apy0)) ltry ltyx).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; apy0)
ltyx: //
(// (y; apy0);
positive_apart_zero (// (y; apy0)) ltry) <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltxy: let apx1 :=
  positive_apart_zero (// (x; apx0))
    (transitivity
       (pos_recip_compat (// (y; apy0)) ltry)
       ltyx) in
// (// (x; apx0); apx1) < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  cbn in ltxy.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; apy0)
ltyx: //
(// (y; apy0);
positive_apart_zero (// (y; apy0)) ltry) <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltxy: //
(// (x; apx0);
positive_apart_zero (// (x; apx0))
  (strictorder_trans 0
     (//
      (// (y; apy0);
      positive_apart_zero (// (y; apy0)) ltry))
     (// (x; apx0))
     (pos_recip_compat (// (y; apy0)) ltry)
     ltyx)) < // (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  rewrite (recip_irrelevant (//(x;apx0)) (positive_apart_zero (// (x; apx0)) (transitivity (pos_recip_compat (// (y; apy0)) ltry) ltyx)) (recip_apart x apx0)) in ltxy.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x, y: F
Px: 0 < x
Py: 0 < y
apy0:= positive_apart_zero y Py: y ≶ 0
ltry: 0 < // (y; apy0)
ltyx: //
(// (y; apy0);
positive_apart_zero (// (y; apy0)) ltry) <
// (x; positive_apart_zero x Px)
apx0:= positive_apart_zero x Px: x ≶ 0
ltxy: // (// (x; apx0); recip_apart x apx0) <
// (y; apy0)
// (// (x; apx0); recip_apart x apx0) < // (y; apy0)
  assumption.
Qed.

Lemma field_split2 (x : F) : (x * recip'  2 (positive_apart_zero 2 lt_0_2)) + (x * recip' 2 (positive_apart_zero 2 lt_0_2)) = x.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x * recip' 2 (positive_apart_zero 2 lt_0_2) +
x * recip' 2 (positive_apart_zero 2 lt_0_2) = x
Proof.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x * recip' 2 (positive_apart_zero 2 lt_0_2) +
x * recip' 2 (positive_apart_zero 2 lt_0_2) = x
  rewrite <- plus_mult_distr_l.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x *
(recip' 2 (positive_apart_zero 2 lt_0_2) +
 recip' 2 (positive_apart_zero 2 lt_0_2)) = x
  rewrite <- (mult_1_l (recip' 2 (positive_apart_zero 2 lt_0_2))).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x *
(1 * recip' 2 (positive_apart_zero 2 lt_0_2) +
 1 * recip' 2 (positive_apart_zero 2 lt_0_2)) = x
  rewrite <- plus_mult_distr_r.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x * (2 * recip' 2 (positive_apart_zero 2 lt_0_2)) = x
  rewrite (recip_inverse' 2 (positive_apart_zero 2 lt_0_2)).
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x * 1 = x
  rewrite mult_1_r.
F: Type
Alt: Lt F
Ale: Le F
Aap: Apart F
Azero: Zero F
Aone: One F
Aplus: Plus F
Anegate: Negate F
Amult: Mult F
Arecip: Recip F
Ajoin: Join F
Ameet: Meet F
H: OrderedField F
x: F
x = x
  reflexivity.
Qed.
End contents.