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

Section cauchy.
  Context (Q : Type).
  Context `{Rationals Q}.
  Context {Q_dec_paths : DecidablePaths Q}.
  Context {Qtriv : TrivialApart Q}.
  Context (F : Type).
  Context `{Forderedfield : OrderedField F}.
  Let qinc : Cast Q F := rationals_to_field Q F.
  Existing Instance qinc.
  (* TODO The following two instances should probably come from the
  `Rationals` instance. *)
  Context (qinc_strong_presving : IsSemiRingStrongPreserving qinc).
  Existing Instance qinc_strong_presving.

  Section sequence.
    Context (x : nat -> F).

    Class CauchyModulus (M : Qpos Q -> nat) :=
      cauchy_convergence : forall epsilon : Qpos Q, forall m n,
            M epsilon <= m -> M epsilon <= n ->
            - ' (' epsilon) < (x m) - (x n) < ' (' epsilon).

    Class IsLimit (l : F) := is_limit
      : forall epsilon : Qpos Q,
          hexists (fun N : nat => forall n : nat, N <= n ->
            - ' (' epsilon) < l - x n < ' (' epsilon)).
  End sequence.

  Class IsComplete := is_complete
    : forall x : nat -> F, forall M , CauchyModulus x M -> exists l, IsLimit x l.

  Section theory.
    Context (x : nat -> F) {M} `{CauchyModulus x M}.

    Lemma modulus_close_limit
          {l}
          (islim : IsLimit x l)
          (epsilon : Qpos Q)
      : x (M (epsilon / 2)) - ' (' epsilon)
        < l
        < x (M (epsilon / 2)) + ' (' epsilon).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
    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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (lim_close := is_limit x (epsilon / 2));
        strip_truncations.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
lim_close: {N : nat &
forall n : nat,
N ≤ n ->
- ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))}
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      destruct lim_close as [N isclose'].
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
isclose': forall n : nat,
N ≤ n ->
- ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      set (n := Nat.Core.max (M (epsilon / 2)) N).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
isclose': forall n : nat,
N ≤ n ->
- ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
n:= Core.max (M (epsilon / 2)) N: nat
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (leNn := le_nat_max_r (M (epsilon / 2)) N : N ≤ n).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
isclose': forall n : nat,
N ≤ n ->
- ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (isclose := isclose' n leNn).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
isclose': forall n : nat,
N ≤ n ->
- ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      clear isclose'.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (leMn := le_nat_max_l (M (epsilon / 2)) N : M (epsilon / 2) ≤ n).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
leMn: M (epsilon / 2) ≤ n
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (leMM : M (epsilon / 2) ≤ M (epsilon / 2) ) by apply (Nat.Core.leq_n).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (x_close := cauchy_convergence x (epsilon/2) n (M (epsilon / 2)) leMn leMM).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' (epsilon / 2)) < 
l - x n < ' (' (epsilon / 2))
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - ' (' (epsilon / 2)) <
x n - x (M (epsilon / 2)) <
' (' (epsilon / 2))
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      cbn in isclose, x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - ' (' epsilon / 2) < l - x n <
' (' epsilon / 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - ' (' epsilon / 2) <
x n - x (M (epsilon / 2)) <
' (' epsilon / 2)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      rewrite (@preserves_mult Q F _ _ _ _ _ _ _ _ _ _ _ _) in isclose, x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (eq22 : ' 2 = 2).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
' 2 = 2
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      {
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
' 2 = 2
        rewrite (@preserves_plus Q F _ _ _ _ _ _ _ _ _ _ _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
' 1 + ' 1 = 2
        rewrite (@preserves_1 Q F _ _ _ _ _ _ _ _ _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
2 = 2
        reflexivity.
      }
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      set (ap20 := positive_apart_zero 2 lt_0_2 : 2 ≶ 0).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (ap20' : ' 2 ≶ 0).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
' 2 ≶ 0
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
ap20': ' 2 ≶ 0
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      {
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
' 2 ≶ 0
        rewrite eq22; exact ap20.
      }
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
isclose: - (' (' epsilon) * ' (/ 2)) < 
l - x n < ' (' epsilon) * ' (/ 2)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) * ' (/ 2)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) * ' (/ 2)
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
ap20': ' 2 ≶ 0
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      rewrite (dec_recip_to_recip 2 ap20') in isclose, x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      assert (eq_recip_22 : recip' (' 2) ap20' = recip' 2 ap20).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
recip' (' 2) ap20' = recip' 2 ap20
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
eq_recip_22: recip' (' 2) ap20' = recip' 2 ap20
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      {
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
recip' (' 2) ap20' = recip' 2 ap20
        apply recip_proper_alt.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
' 2 = 2
        exact eq22.
      }
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
eq_recip_22: recip' (' 2) ap20' = recip' 2 ap20
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      unfold recip' in eq_recip_22.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
isclose: - (' (' epsilon) // (' 2; ap20')) <
l - x n < ' (' epsilon) // (' 2; ap20')
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (' 2; ap20')) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (' 2; ap20')
eq22: ' 2 = 2
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
eq_recip_22: // (' 2; ap20') = // (2; ap20)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      rewrite eq_recip_22 in isclose, x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20': ' 2 ≶ 0
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eq22: ' 2 = 2
eq_recip_22: // (' 2; ap20') = // (2; ap20)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      clear eq22 ap20' eq_recip_22.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
x (M (epsilon / 2)) - ' (' epsilon) < l <
x (M (epsilon / 2)) + ' (' epsilon)
      rewrite <- (field_split2 (' (' epsilon))).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
x (M (epsilon / 2)) -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
x (M (epsilon / 2)) +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      set (eps_recip_2 := (' (' epsilon) * recip' 2 ap20)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) * recip' 2 ap20: F
x (M (epsilon / 2)) -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
x (M (epsilon / 2)) +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      fold ap20.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) * recip' 2 ap20: F
x (M (epsilon / 2)) -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
x (M (epsilon / 2)) +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      change (' (' epsilon) * recip' 2 ap20) with eps_recip_2.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) * recip' 2 ap20: F
x (M (epsilon / 2)) -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
x (M (epsilon / 2)) +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      unfold recip' in eps_recip_2.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x (M (epsilon / 2)) -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
x (M (epsilon / 2)) +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      set (xMeps2 := x (M (epsilon / 2))).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
x_close: - (' (' epsilon) // (2; ap20)) <
x n - x (M (epsilon / 2)) <
' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2:= x (M (epsilon / 2)): F
xMeps2 -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      fold xMeps2 in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 -
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      rewrite negate_plus_distr.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      split.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
l <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
      -
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) < l apply (strictly_order_reflecting (+ (- x n))).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
l - x n
        refine (transitivity _ (fst isclose)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- (' (' epsilon) // (2; ap20))
        clear isclose.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- (' (' epsilon) // (2; ap20))
        fold eps_recip_2.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        fold eps_recip_2 in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: - eps_recip_2 < x n - xMeps2 < eps_recip_2
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        apply fst, flip_lt_minus_r in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: - eps_recip_2 + xMeps2 < x n
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        rewrite plus_comm in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - eps_recip_2 < x n
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        apply flip_lt_minus_l in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 < x n + eps_recip_2
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        rewrite plus_comm in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 < eps_recip_2 + x n
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        apply flip_lt_minus_l in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n <
- eps_recip_2
        rewrite <-(plus_assoc xMeps2 _ (- x n)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) - x n) <
- eps_recip_2
        rewrite (plus_comm _ (- x n)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 +
(- x n +
 (-
  (' (' epsilon) *
   recip' 2 (positive_apart_zero 2 lt_0_2)) -
  ' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2))) <
- eps_recip_2
        rewrite (plus_assoc xMeps2 (- x n) _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) <
- eps_recip_2
        apply (strictly_order_reflecting (+ eps_recip_2)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) +
eps_recip_2 < - eps_recip_2 + eps_recip_2
        apply (strictly_order_reflecting (+ eps_recip_2)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) +
eps_recip_2 + eps_recip_2 <
- eps_recip_2 + eps_recip_2 + eps_recip_2
        rewrite plus_negate_l, plus_0_l.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) +
eps_recip_2 + eps_recip_2 < eps_recip_2
        rewrite <- (plus_assoc (xMeps2 - x n) _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(-
 (' (' epsilon) *
  recip' 2 (positive_apart_zero 2 lt_0_2)) -
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) + eps_recip_2) +
eps_recip_2 < eps_recip_2
        rewrite <- (plus_assoc (-eps_recip_2) _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n +
(- eps_recip_2 +
 (-
  (' (' epsilon) *
   recip' 2 (positive_apart_zero 2 lt_0_2)) +
  eps_recip_2)) + eps_recip_2 < eps_recip_2
        rewrite plus_negate_l, plus_0_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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n - eps_recip_2 + eps_recip_2 < eps_recip_2
        rewrite <- (plus_assoc (xMeps2 - x n) _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n + (- eps_recip_2 + eps_recip_2) <
eps_recip_2
        rewrite plus_negate_l, plus_0_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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: xMeps2 - x n < eps_recip_2
xMeps2 - x n < eps_recip_2
        assumption.
      -
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
l <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) apply (strictly_order_reflecting (+ (- x n))).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
l - x n <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        refine (transitivity (snd isclose) _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
isclose: - (' (' epsilon) // (2; ap20)) < 
l - x n < ' (' epsilon) // (2; ap20)
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
' (' epsilon) // (2; ap20) <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        clear isclose.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
' (' epsilon) // (2; ap20) <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        fold eps_recip_2.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
x_close: - (' (' epsilon) // (2; ap20)) <
x n - xMeps2 < ' (' epsilon) // (2; ap20)
eps_recip_2:= ' (' epsilon) // (2; ap20): F
eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        fold eps_recip_2 in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: - eps_recip_2 < x n - xMeps2 < eps_recip_2
eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        apply snd in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n - xMeps2 < eps_recip_2
eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        apply flip_lt_minus_l in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < eps_recip_2 + xMeps2
eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        rewrite plus_comm in x_close.
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n
        apply (strictly_order_reflecting (+ x n)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
eps_recip_2 + x n <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) - x n + 
x n
        rewrite <- (plus_assoc _ (-x n) (x n)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
eps_recip_2 + x n <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2)) +
(- x n + x n)
        rewrite plus_negate_l, plus_0_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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
eps_recip_2 + x n <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
        rewrite (plus_comm eps_recip_2 (x n)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
x n + eps_recip_2 <
xMeps2 +
(' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2) +
 ' (' epsilon) *
 recip' 2 (positive_apart_zero 2 lt_0_2))
        rewrite (plus_assoc xMeps2 _ _).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
x n + eps_recip_2 <
xMeps2 +
' (' epsilon) *
recip' 2 (positive_apart_zero 2 lt_0_2) +
' (' epsilon) *
recip' 2 (positive_apart_zero 2 lt_0_2)
        apply (strictly_order_preserving (+ eps_recip_2)).
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
Q_dec_paths: DecidablePaths Q
Qtriv: TrivialApart 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
Forderedfield: OrderedField F
qinc:= rationals_to_field Q F: Cast Q F
qinc_strong_presving: IsSemiRingStrongPreserving qinc
x: nat -> F
M: Qpos Q -> nat
H0: CauchyModulus x M
l: F
islim: IsLimit x l
epsilon: Qpos Q
N: nat
n:= Core.max (M (epsilon / 2)) N: nat
leNn: N ≤ n
ap20:= positive_apart_zero 2 lt_0_2 : 2 ≶ 0: 2 ≶ 0
leMn: M (epsilon / 2) ≤ n
leMM: M (epsilon / 2) ≤ M (epsilon / 2)
xMeps2:= x (M (epsilon / 2)): F
eps_recip_2:= ' (' epsilon) // (2; ap20): F
x_close: x n < xMeps2 + eps_recip_2
x n <
xMeps2 +
' (' epsilon) *
recip' 2 (positive_apart_zero 2 lt_0_2)
        assumption.
    Qed.

  End theory.

End cauchy.