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

Generalizable Variables Q F.

Section strict_field_order.
  Context `{Rationals Q}.
  Context {Qmeet} {Qjoin} `{@LatticeOrder Q (_ : Le Q) Qmeet Qjoin}.
  Context `{OrderedField F}.
  Context {archim : ArchimedeanProperty Q F}.

  Definition qinc : Cast Q F := rationals_to_field Q F.
  Existing Instance qinc.

  Lemma char_minus_left x y : - x < y -> - y < x.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
- x < y -> - y < x
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
- x < y -> - y < x
    intros ltnxy.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: - x < y
- y < x rewrite <- (negate_involutive x).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: - x < y
- y < - - x apply (snd (flip_lt_negate _ _)).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: - x < y
- x < y assumption.
  Qed.

  Lemma char_minus_right x y : x < - y -> y < - x.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
x < - y -> y < - x
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
x < - y -> y < - x
    intros ltnxy.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: x < - y
y < - x rewrite <- (negate_involutive y).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: x < - y
- - y < - x apply (snd (flip_lt_negate _ _)).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
x, y: F
ltnxy: x < - y
x < - y assumption.
  Qed.

  Lemma char_plus_left : forall (q : Q) (x y : F),
      ' q < x + y <-> hexists (fun s : Q => (' s < x) /\ (' (q - s) < y)).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x + y <->
hexists
  (fun s : Q => ((' s < x) * (' (q - s) < y))%type)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x + y <->
hexists
  (fun s : Q => ((' s < x) * (' (q - s) < y))%type) Abort.
  Lemma char_plus_right : forall (r : Q) (x y : F),
      x + y < ' r <-> hexists (fun t : Q => (x < ' t) /\ (y < ' (r - t))).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x + y < ' r <->
hexists
  (fun t : Q => ((x < ' t) * (y < ' (r - t)))%type)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x + y < ' r <->
hexists
  (fun t : Q => ((x < ' t) * (y < ' (r - t)))%type) Abort.

  Definition hexists4 {X Y Z W} (f : X -> Y -> Z -> W -> Type) : HProp
    := hexists (fun xyzw => match xyzw with
                            | ((x , y) , (z , w)) => f x y z w
                            end).

  Lemma char_times_left : forall (q : Q) (x y : F),
          ' q < x * y
      <-> hexists4 (fun a b c d : Q =>
                      (q < meet (meet a b) (meet c d))
                      /\
                      ((' a < x < ' b)
                       /\
                       (' c < y < ' d)
                      )
                   ).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x * y <->
hexists4
  (fun a b c d : Q =>
   ((q < (a ⊓ b) ⊓ (c ⊓ d)) *
    ((' a < x < ' b) * (' c < y < ' d)))%type)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x * y <->
hexists4
  (fun a b c d : Q =>
   ((q < (a ⊓ b) ⊓ (c ⊓ d)) *
    ((' a < x < ' b) * (' c < y < ' d)))%type) Abort.
  Lemma char_times_right : forall (r : Q) (x y : F),
          x * y < ' r
      <-> hexists4 (fun a b c d : Q =>
                      and (join (join a b) (join c d) < r)
                          (and
                             (' a < x < ' b)
                             (' c < y < ' d)
                          )
                   ).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x * y < ' r <->
hexists4
  (fun a b c d : Q =>
   (((a ⊔ b) ⊔ (c ⊔ d) < r) *
    ((' a < x < ' b) * (' c < y < ' d)))%type)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x * y < ' r <->
hexists4
  (fun a b c d : Q =>
   (((a ⊔ b) ⊔ (c ⊔ d) < r) *
    ((' a < x < ' b) * (' c < y < ' d)))%type) Abort.
  Lemma char_recip_pos_left : forall (q : Q) (z : F) (nu : 0 < z),
    'q < recip' z (positive_apart_zero z nu) <-> ' q * z < 1.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (z : F) (nu : 0 < z),
' q < recip' z (positive_apart_zero z nu) <->
' q * z < 1
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (z : F) (nu : 0 < z),
' q < recip' z (positive_apart_zero z nu) <->
' q * z < 1 Abort.
  Lemma char_recip_pos_right : forall (r : Q) (z : F) (nu : 0 < z),
    recip' z (positive_apart_zero z nu) < ' r <-> 1 < ' r * z.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (z : F) (nu : 0 < z),
recip' z (positive_apart_zero z nu) < ' r <->
1 < ' r * z
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (z : F) (nu : 0 < z),
recip' z (positive_apart_zero z nu) < ' r <->
1 < ' r * z Abort.
  Lemma char_recip_neg_left : forall (q : Q) (w : F) (nu : w < 0),
    'q < recip' w (negative_apart_zero w nu) <-> ' q * w < 1.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (w : F) (nu : w < 0),
' q < recip' w (negative_apart_zero w nu) <->
' q * w < 1
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (w : F) (nu : w < 0),
' q < recip' w (negative_apart_zero w nu) <->
' q * w < 1 Abort.
  Lemma char_recip_neg_right : forall (r : Q) (w : F) (nu : w < 0),
    recip' w (negative_apart_zero w nu) < ' r <-> ' r * w < 1.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (w : F) (nu : w < 0),
recip' w (negative_apart_zero w nu) < ' r <->
' r * w < 1
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (w : F) (nu : w < 0),
recip' w (negative_apart_zero w nu) < ' r <->
' r * w < 1 Abort.

  Lemma char_meet_left : forall (q : Q) (x y : F),
      ' q < meet x y <-> ' q < x /\ ' q < y.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x ⊓ y <-> (' q < x) * (' q < y)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x ⊓ y <-> (' q < x) * (' q < y) Abort.
  Lemma char_meet_right : forall (r : Q) (x y : F),
      meet x y < 'r <-> hor (x < 'r) (y < 'r).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x ⊓ y < ' r <-> hor (x < ' r) (y < ' r)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x ⊓ y < ' r <-> hor (x < ' r) (y < ' r) Abort.
  Lemma char_join_left : forall (q : Q) (x y : F),
      ' q < join x y <-> hor ('q < x) ('q < y).
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x ⊔ y <-> hor (' q < x) (' q < y)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (q : Q) (x y : F),
' q < x ⊔ y <-> hor (' q < x) (' q < y) Abort.
  Lemma char_join_right : forall (r : Q) (x y : F),
      join x y < ' r <-> x < ' r /\ y < ' r.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x ⊔ y < ' r <-> (x < ' r) * (y < ' r)
  Proof.
Q: Type
Aap: Apart Q
Aplus: Plus Q
Amult: Mult Q
Azero: Zero Q
Aone: One Q
Aneg: Negate Q
Arecip: DecRecip Q
Ale: Le Q
Alt: Lt Q
U: RationalsToField Q
H: Rationals Q
Qmeet: Meet Q
Qjoin: Join Q
H0: LatticeOrder (Ale : Le Q)
F: Type
Alt0: Lt F
Ale0: Le F
Aap0: Apart F
Azero0: Zero F
Aone0: One F
Aplus0: Plus F
Anegate: Negate F
Amult0: Mult F
Arecip0: Recip F
Ajoin: Join F
Ameet: Meet F
H1: OrderedField F
archim: ArchimedeanProperty Q F
forall (r : Q) (x y : F),
x ⊔ y < ' r <-> (x < ' r) * (y < ' r) Abort.

End strict_field_order.