Library Flocq.Appli.Fappli_double_round

Conditions for innocuous double rounding.


Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_generic_fmt.
Require Import Fcalc_ops.
Require Import Fcore_ulp.

Require Import Psatz.

Open Scope R_scope.

Section Double_round.

Variable beta : radix.
Notation bpow e := (bpow beta e).
Notation ln_beta x := (ln_beta beta x).

Definition double_round_eq fexp1 fexp2 choice1 choice2 x :=
  round beta fexp1 (Znearest choice1) (round beta fexp2 (Znearest choice2) x)
  = round beta fexp1 (Znearest choice1) x.

A little tactic to simplify terms of the form bpow a × bpow b.
Ltac bpow_simplify :=
  
  repeat
    match goal with
      | |- context [(Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
        rewrite <- bpow_plus
      | |- context [(?X1 × Fcore_Raux.bpow _ _ × Fcore_Raux.bpow _ _)] ⇒
        rewrite (Rmult_assoc X1); rewrite <- bpow_plus
      | |- context [(?X1 × (?X2 × Fcore_Raux.bpow _ _) × Fcore_Raux.bpow _ _)] ⇒
        rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
        rewrite <- bpow_plus
    end;
  
  repeat
    match goal with
      | |- context [(Fcore_Raux.bpow _ ?X)] ⇒
        progress ring_simplify X
    end;
  
  change (Fcore_Raux.bpow _ 0) with 1;
  repeat
    match goal with
      | |- context [(_ × 1)] ⇒
        rewrite Rmult_1_r
    end.

Definition midp (fexp : ZZ) (x : R) :=
  round beta fexp Zfloor x + / 2 × ulp beta fexp x.

Definition midp' (fexp : ZZ) (x : R) :=
  round beta fexp Zceil x - / 2 × ulp beta fexp x.

Lemma double_round_lt_mid_further_place' :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x
  x < midp fexp1 x - / 2 × ulp beta fexp2 x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_lt_mid_further_place :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  x < midp fexp1 x - / 2 × ulp beta fexp2 x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_lt_mid_same_place :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z
  x < midp fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_lt_mid :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x))%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  x < midp fexp1 x
  ((fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
   x < midp fexp1 x - / 2 × ulp beta fexp2 x) →
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_gt_mid_further_place' :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  round beta fexp2 (Znearest choice2) x < bpow (ln_beta x) →
  midp' fexp1 x + / 2 × ulp beta fexp2 x < x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_gt_mid_further_place :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  midp' fexp1 x + / 2 × ulp beta fexp2 x < x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_gt_mid_same_place :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) = fexp1 (ln_beta x))%Z
  midp' fexp1 x < x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_gt_mid :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x))%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  midp' fexp1 x < x
  ((fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
   midp' fexp1 x + / 2 × ulp beta fexp2 x < x) →
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Section Double_round_mult.

Lemma ln_beta_mult_disj :
   x y,
  x 0 → y 0 →
  ((ln_beta (x × y) = (ln_beta x + ln_beta y - 1)%Z :> Z)
    (ln_beta (x × y) = (ln_beta x + ln_beta y)%Z :> Z)).

Definition double_round_mult_hyp fexp1 fexp2 :=
  ( ex ey, (fexp2 (ex + ey) fexp1 ex + fexp1 ey)%Z)
   ( ex ey, (fexp2 (ex + ey - 1) fexp1 ex + fexp1 ey)%Z).

Lemma double_round_mult_aux :
   (fexp1 fexp2 : ZZ),
  double_round_mult_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x × y).

Variable rnd : RZ.
Context { valid_rnd : Valid_rnd rnd }.

Theorem double_round_mult :
   (fexp1 fexp2 : ZZ),
  double_round_mult_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  round beta fexp1 rnd (round beta fexp2 rnd (x × y))
  = round beta fexp1 rnd (x × y).

Section Double_round_mult_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Theorem double_round_mult_FLX :
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec xFLX_format beta prec y
  round beta (FLX_exp prec) rnd (round beta (FLX_exp prec') rnd (x × y))
  = round beta (FLX_exp prec) rnd (x × y).

End Double_round_mult_FLX.

Section Double_round_mult_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Theorem double_round_mult_FLT :
  (emin' 2 × emin)%Z → (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec xFLT_format beta emin prec y
  round beta (FLT_exp emin prec) rnd
        (round beta (FLT_exp emin' prec') rnd (x × y))
  = round beta (FLT_exp emin prec) rnd (x × y).

End Double_round_mult_FLT.

Section Double_round_mult_FTZ.

Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Theorem double_round_mult_FTZ :
  (emin' + prec' 2 × emin + prec)%Z
  (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  round beta (FTZ_exp emin prec) rnd
        (round beta (FTZ_exp emin' prec') rnd (x × y))
  = round beta (FTZ_exp emin prec) rnd (x × y).

End Double_round_mult_FTZ.

End Double_round_mult.

Section Double_round_plus.

Lemma ln_beta_plus_disj :
   x y,
  0 < yy x
  ((ln_beta (x + y) = ln_beta x :> Z)
    (ln_beta (x + y) = (ln_beta x + 1)%Z :> Z)).

Lemma ln_beta_plus_separated :
   fexp : ZZ,
   x y,
  0 < x → 0 y
  generic_format beta fexp x
  (ln_beta y fexp (ln_beta x))%Z
  (ln_beta (x + y) = ln_beta x :> Z).

Lemma ln_beta_minus_disj :
   x y,
  0 < x → 0 < y
  (ln_beta y ln_beta x - 2)%Z
  ((ln_beta (x - y) = ln_beta x :> Z)
    (ln_beta (x - y) = (ln_beta x - 1)%Z :> Z)).

Lemma ln_beta_minus_separated :
   fexp : ZZ, Valid_exp fexp
   x y,
  0 < x → 0 < yy < x
  bpow (ln_beta x - 1) < x
  generic_format beta fexp x → (ln_beta y fexp (ln_beta x))%Z
  (ln_beta (x - y) = ln_beta x :> Z).

Definition double_round_plus_hyp fexp1 fexp2 :=
  ( ex ey, (fexp1 (ex + 1) - 1 ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 (ex - 1) + 1 ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 ex - 1 ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (ex - 1 ey)%Z → (fexp2 ex fexp1 ey)%Z).

Lemma double_round_plus_aux0_aux_aux :
   (fexp1 fexp2 : ZZ),
   x y,
  (fexp1 (ln_beta x) fexp1 (ln_beta y))%Z
  (fexp2 (ln_beta (x + y))%Z fexp1 (ln_beta x))%Z
  (fexp2 (ln_beta (x + y))%Z fexp1 (ln_beta y))%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma double_round_plus_aux0_aux :
   (fexp1 fexp2 : ZZ),
   x y,
  (fexp2 (ln_beta (x + y))%Z fexp1 (ln_beta x))%Z
  (fexp2 (ln_beta (x + y))%Z fexp1 (ln_beta y))%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma double_round_plus_aux0 :
   (fexp1 fexp2 : ZZ), Valid_exp fexp1
  double_round_plus_hyp fexp1 fexp2
   x y,
  (0 < x)%R → (0 < y)%R → (y x)%R
  (fexp1 (ln_beta x) - 1 ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma double_round_plus_aux1_aux :
   k, (0 < k)%Z
   (fexp : ZZ),
   x y,
  0 < x → 0 < y
  (ln_beta y fexp (ln_beta x) - k)%Z
  (ln_beta (x + y) = ln_beta x :> Z) →
  generic_format beta fexp x
  0 < (x + y) - round beta fexp Zfloor (x + y) < bpow (fexp (ln_beta x) - k).

Lemma double_round_plus_aux1 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  (ln_beta y fexp1 (ln_beta x) - 2)%Z
  generic_format beta fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).
Lemma double_round_plus_aux2 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < x → 0 < yy x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_plus_aux :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 x → 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_minus_aux0_aux :
   (fexp1 fexp2 : ZZ),
   x y,
  (fexp2 (ln_beta (x - y))%Z fexp1 (ln_beta x))%Z
  (fexp2 (ln_beta (x - y))%Z fexp1 (ln_beta y))%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma double_round_minus_aux0 :
   (fexp1 fexp2 : ZZ),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (fexp1 (ln_beta x) - 1 ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma double_round_minus_aux1 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (ln_beta y fexp1 (ln_beta x) - 2)%Z
  (fexp1 (ln_beta (x - y)) - 1 ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma double_round_minus_aux2_aux :
   (fexp : ZZ),
  Valid_exp fexp
   x y,
  0 < yy < x
  (ln_beta y fexp (ln_beta x) - 1)%Z
  generic_format beta fexp x
  generic_format beta fexp y
  round beta fexp Zceil (x - y) - (x - y) y.

Lemma double_round_minus_aux2 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (ln_beta y fexp1 (ln_beta x) - 2)%Z
  (ln_beta y fexp1 (ln_beta (x - y)) - 2)%Z
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_minus_aux3 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 < yy x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_minus_aux :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  0 x → 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_plus :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_minus :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Section Double_round_plus_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLX_double_round_plus_hyp :
  (2 × prec + 1 prec')%Z
  double_round_plus_hyp (FLX_exp prec) (FLX_exp prec').

Theorem double_round_plus_FLX :
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x y,
  FLX_format beta prec xFLX_format beta prec y
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).

Theorem double_round_minus_FLX :
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x y,
  FLX_format beta prec xFLX_format beta prec y
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).

End Double_round_plus_FLX.

Section Double_round_plus_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLT_double_round_plus_hyp :
  (emin' emin)%Z → (2 × prec + 1 prec')%Z
  double_round_plus_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem double_round_plus_FLT :
   choice1 choice2,
  (emin' emin)%Z → (2 × prec + 1 prec')%Z
   x y,
  FLT_format beta emin prec xFLT_format beta emin prec y
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem double_round_minus_FLT :
   choice1 choice2,
  (emin' emin)%Z → (2 × prec + 1 prec')%Z
   x y,
  FLT_format beta emin prec xFLT_format beta emin prec y
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_FLT.

Section Double_round_plus_FTZ.

Require Import Fcore_FLX.
Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FTZ_double_round_plus_hyp :
  (emin' + prec' emin + 1)%Z → (2 × prec + 1 prec')%Z
  double_round_plus_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem double_round_plus_FTZ :
   choice1 choice2,
  (emin' + prec' emin + 1)%Z → (2 × prec + 1 prec')%Z
   x y,
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem double_round_minus_FTZ :
   choice1 choice2,
  (emin' + prec' emin + 1)%Z → (2 × prec + 1 prec')%Z
   x y,
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_FTZ.

Section Double_round_plus_beta_ge_3.

Definition double_round_plus_beta_ge_3_hyp fexp1 fexp2 :=
  ( ex ey, (fexp1 (ex + 1) ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 (ex - 1) + 1 ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (fexp1 ex ey)%Z → (fexp2 ex fexp1 ey)%Z)
   ( ex ey, (ex - 1 ey)%Z → (fexp2 ex fexp1 ey)%Z).

Lemma double_round_plus_beta_ge_3_aux0 :
   (fexp1 fexp2 : ZZ), Valid_exp fexp1
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  (0 < y)%R → (y x)%R
  (fexp1 (ln_beta x) ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x + y).

Lemma double_round_plus_beta_ge_3_aux1 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  (ln_beta y fexp1 (ln_beta x) - 1)%Z
  generic_format beta fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_plus_beta_ge_3_aux2 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < yy x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_plus_beta_ge_3_aux :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 x → 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_minus_beta_ge_3_aux0 :
   (fexp1 fexp2 : ZZ),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (fexp1 (ln_beta x) ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma double_round_minus_beta_ge_3_aux1 :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (ln_beta y fexp1 (ln_beta x) - 1)%Z
  (fexp1 (ln_beta (x - y)) ln_beta y)%Z
  generic_format beta fexp1 xgeneric_format beta fexp1 y
  generic_format beta fexp2 (x - y).

Lemma double_round_minus_beta_ge_3_aux2 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < yy < x
  (ln_beta y fexp1 (ln_beta x) - 1)%Z
  (ln_beta y fexp1 (ln_beta (x - y)) - 1)%Z
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_minus_beta_ge_3_aux3 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 < yy x
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_minus_beta_ge_3_aux :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  0 x → 0 y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Lemma double_round_plus_beta_ge_3 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x + y).

Lemma double_round_minus_beta_ge_3 :
  (3 beta)%Z
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_plus_beta_ge_3_hyp fexp1 fexp2
   x y,
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x - y).

Section Double_round_plus_beta_ge_3_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLX_double_round_plus_beta_ge_3_hyp :
  (2 × prec prec')%Z
  double_round_plus_beta_ge_3_hyp (FLX_exp prec) (FLX_exp prec').

Theorem double_round_plus_beta_ge_3_FLX :
  (3 beta)%Z
   choice1 choice2,
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec xFLX_format beta prec y
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x + y).

Theorem double_round_minus_beta_ge_3_FLX :
  (3 beta)%Z
   choice1 choice2,
  (2 × prec prec')%Z
   x y,
  FLX_format beta prec xFLX_format beta prec y
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x - y).

End Double_round_plus_beta_ge_3_FLX.

Section Double_round_plus_beta_ge_3_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLT_double_round_plus_beta_ge_3_hyp :
  (emin' emin)%Z → (2 × prec prec')%Z
  double_round_plus_beta_ge_3_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem double_round_plus_beta_ge_3_FLT :
  (3 beta)%Z
   choice1 choice2,
  (emin' emin)%Z → (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec xFLT_format beta emin prec y
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem double_round_minus_beta_ge_3_FLT :
  (3 beta)%Z
   choice1 choice2,
  (emin' emin)%Z → (2 × prec prec')%Z
   x y,
  FLT_format beta emin prec xFLT_format beta emin prec y
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_beta_ge_3_FLT.

Section Double_round_plus_beta_ge_3_FTZ.

Require Import Fcore_FLX.
Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FTZ_double_round_plus_beta_ge_3_hyp :
  (emin' + prec' emin + 1)%Z → (2 × prec prec')%Z
  double_round_plus_beta_ge_3_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem double_round_plus_beta_ge_3_FTZ :
  (3 beta)%Z
   choice1 choice2,
  (emin' + prec' emin + 1)%Z → (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x + y).

Theorem double_round_minus_beta_ge_3_FTZ :
  (3 beta)%Z
   choice1 choice2,
  (emin' + prec' emin + 1)%Z → (2 × prec prec')%Z
   x y,
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x - y).

End Double_round_plus_beta_ge_3_FTZ.

End Double_round_plus_beta_ge_3.

End Double_round_plus.

Lemma double_round_mid_cases :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  (Rabs (x - midp fexp1 x) / 2 × (ulp beta fexp2 x)
   double_round_eq fexp1 fexp2 choice1 choice2 x) →
  double_round_eq fexp1 fexp2 choice1 choice2 x.
Section Double_round_sqrt.

Definition double_round_sqrt_hyp fexp1 fexp2 :=
  ( ex, (2 × fexp1 ex fexp1 (2 × ex))%Z)
   ( ex, (2 × fexp1 ex fexp1 (2 × ex - 1))%Z)
   ( ex, (fexp1 (2 × ex) < 2 × ex)%Z
                 (fexp2 ex + ex 2 × fexp1 ex - 2)%Z).

Lemma ln_beta_sqrt_disj :
   x,
  0 < x
  (ln_beta x = 2 × ln_beta (sqrt x) - 1 :> Z)%Z
   (ln_beta x = 2 × ln_beta (sqrt x) :> Z)%Z.

Lemma double_round_sqrt_aux :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
  double_round_sqrt_hyp fexp1 fexp2
   x,
  0 < x
  (fexp2 (ln_beta (sqrt x)) fexp1 (ln_beta (sqrt x)) - 1)%Z
  generic_format beta fexp1 x
  / 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).

Lemma sqrt_neg : x, x 0 → sqrt x = 0.

Lemma double_round_sqrt :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_sqrt_hyp fexp1 fexp2
   x,
  generic_format beta fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).

Section Double_round_sqrt_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLX_double_round_sqrt_hyp :
  (2 × prec + 2 prec')%Z
  double_round_sqrt_hyp (FLX_exp prec) (FLX_exp prec').

Theorem double_round_sqrt_FLX :
   choice1 choice2,
  (2 × prec + 2 prec')%Z
   x,
  FLX_format beta prec x
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).

End Double_round_sqrt_FLX.

Section Double_round_sqrt_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLT_double_round_sqrt_hyp :
  (emin 0)%Z
  ((emin' emin - prec - 2)%Z
    (2 × emin' emin - 4 × prec - 2)%Z) →
  (2 × prec + 2 prec')%Z
  double_round_sqrt_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem double_round_sqrt_FLT :
   choice1 choice2,
  (emin 0)%Z
  ((emin' emin - prec - 2)%Z
    (2 × emin' emin - 4 × prec - 2)%Z) →
  (2 × prec + 2 prec')%Z
   x,
  FLT_format beta emin prec x
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_FLT.

Section Double_round_sqrt_FTZ.

Require Import Fcore_FLX.
Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FTZ_double_round_sqrt_hyp :
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 2 prec')%Z
  double_round_sqrt_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem double_round_sqrt_FTZ :
  (4 beta)%Z
   choice1 choice2,
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 2 prec')%Z
   x,
  FTZ_format beta emin prec x
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_FTZ.

Section Double_round_sqrt_beta_ge_4.

Definition double_round_sqrt_beta_ge_4_hyp fexp1 fexp2 :=
  ( ex, (2 × fexp1 ex fexp1 (2 × ex))%Z)
   ( ex, (2 × fexp1 ex fexp1 (2 × ex - 1))%Z)
   ( ex, (fexp1 (2 × ex) < 2 × ex)%Z
                 (fexp2 ex + ex 2 × fexp1 ex - 1)%Z).

Lemma double_round_sqrt_beta_ge_4_aux :
  (4 beta)%Z
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
  double_round_sqrt_beta_ge_4_hyp fexp1 fexp2
   x,
  0 < x
  (fexp2 (ln_beta (sqrt x)) fexp1 (ln_beta (sqrt x)) - 1)%Z
  generic_format beta fexp1 x
  / 2 × ulp beta fexp2 (sqrt x) < Rabs (sqrt x - midp fexp1 (sqrt x)).

Lemma double_round_sqrt_beta_ge_4 :
  (4 beta)%Z
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_sqrt_beta_ge_4_hyp fexp1 fexp2
   x,
  generic_format beta fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 (sqrt x).

Section Double_round_sqrt_beta_ge_4_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLX_double_round_sqrt_beta_ge_4_hyp :
  (2 × prec + 1 prec')%Z
  double_round_sqrt_beta_ge_4_hyp (FLX_exp prec) (FLX_exp prec').

Theorem double_round_sqrt_beta_ge_4_FLX :
  (4 beta)%Z
   choice1 choice2,
  (2 × prec + 1 prec')%Z
   x,
  FLX_format beta prec x
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (sqrt x).

End Double_round_sqrt_beta_ge_4_FLX.

Section Double_round_sqrt_beta_ge_4_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLT_double_round_sqrt_beta_ge_4_hyp :
  (emin 0)%Z
  ((emin' emin - prec - 1)%Z
    (2 × emin' emin - 4 × prec)%Z) →
  (2 × prec + 1 prec')%Z
  double_round_sqrt_beta_ge_4_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem double_round_sqrt_beta_ge_4_FLT :
  (4 beta)%Z
   choice1 choice2,
  (emin 0)%Z
  ((emin' emin - prec - 1)%Z
    (2 × emin' emin - 4 × prec)%Z) →
  (2 × prec + 1 prec')%Z
   x,
  FLT_format beta emin prec x
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_beta_ge_4_FLT.

Section Double_round_sqrt_beta_ge_4_FTZ.

Require Import Fcore_FLX.
Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FTZ_double_round_sqrt_beta_ge_4_hyp :
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 1 prec')%Z
  double_round_sqrt_beta_ge_4_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem double_round_sqrt_beta_ge_4_FTZ :
  (4 beta)%Z
   choice1 choice2,
  (2 × (emin' + prec') emin + prec 1)%Z
  (2 × prec + 1 prec')%Z
   x,
  FTZ_format beta emin prec x
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (sqrt x).

End Double_round_sqrt_beta_ge_4_FTZ.

End Double_round_sqrt_beta_ge_4.

End Double_round_sqrt.

Section Double_round_div.

Lemma double_round_eq_mid_beta_even :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  ( n, (beta = 2 × n :> Z)%Z) →
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  (fexp1 (ln_beta x) ln_beta x)%Z
  x = midp fexp1 x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_really_zero :
   (fexp1 fexp2 : ZZ),
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (ln_beta x fexp1 (ln_beta x) - 2)%Z
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_zero :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z
  x < bpow (ln_beta x) - / 2 × ulp beta fexp2 x
  double_round_eq fexp1 fexp2 choice1 choice2 x.

Lemma double_round_all_mid_cases :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
   x,
  0 < x
  (fexp2 (ln_beta x) fexp1 (ln_beta x) - 1)%Z
  ((fexp1 (ln_beta x) = ln_beta x + 1 :> Z)%Z
   bpow (ln_beta x) - / 2 × ulp beta fexp2 x x
   double_round_eq fexp1 fexp2 choice1 choice2 x) →
  ((fexp1 (ln_beta x) ln_beta x)%Z
   midp fexp1 x - / 2 × ulp beta fexp2 x x < midp fexp1 x
   double_round_eq fexp1 fexp2 choice1 choice2 x) →
  ((fexp1 (ln_beta x) ln_beta x)%Z
   x = midp fexp1 x
   double_round_eq fexp1 fexp2 choice1 choice2 x) →
  ((fexp1 (ln_beta x) ln_beta x)%Z
   midp fexp1 x < x midp fexp1 x + / 2 × ulp beta fexp2 x
   double_round_eq fexp1 fexp2 choice1 choice2 x) →
  double_round_eq fexp1 fexp2 choice1 choice2 x.
Lemma ln_beta_div_disj :
   x y : R,
  0 < x → 0 < y
  ((ln_beta (x / y) = ln_beta x - ln_beta y :> Z)%Z
    (ln_beta (x / y) = ln_beta x - ln_beta y + 1 :> Z)%Z).

Definition double_round_div_hyp fexp1 fexp2 :=
  ( ex, (fexp2 ex fexp1 ex - 1)%Z)
   ( ex ey, (fexp1 ex < ex)%Z → (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) ex - ey + 1)%Z
                    (fexp2 (ex - ey) fexp1 ex - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z → (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey + 1) ex - ey + 1 + 1)%Z
                    (fexp2 (ex - ey + 1) fexp1 ex - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z → (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) ex - ey)%Z
                    (fexp2 (ex - ey) fexp1 (ex - ey)
                                        + fexp1 ey - ey)%Z)
   ( ex ey, (fexp1 ex < ex)%Z → (fexp1 ey < ey)%Z
                    (fexp1 (ex - ey) = ex - ey + 1)%Z
                    (fexp2 (ex - ey) ex - ey - ey + fexp1 ey)%Z).

Lemma double_round_div_aux0 :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_div_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  fexp1 (ln_beta (x / y)) = (ln_beta (x / y) + 1)%Z
  ¬ (bpow (ln_beta (x / y)) - / 2 × ulp beta fexp2 (x / y) x / y).

Lemma double_round_div_aux1 :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_div_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  (fexp1 (ln_beta (x / y)) ln_beta (x / y))%Z
  ¬ (midp fexp1 (x / y) - / 2 × ulp beta fexp2 (x / y)
      x / y
     < midp fexp1 (x / y)).

Lemma double_round_div_aux2 :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  double_round_div_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  (fexp1 (ln_beta (x / y)) ln_beta (x / y))%Z
  ¬ (midp fexp1 (x / y)
     < x / y
      midp fexp1 (x / y) + / 2 × ulp beta fexp2 (x / y)).

Lemma double_round_div_aux :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  ( n, (beta = 2 × n :> Z)%Z) →
  double_round_div_hyp fexp1 fexp2
   x y,
  0 < x → 0 < y
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x / y).

Lemma double_round_div :
   fexp1 fexp2 : ZZ,
  Valid_exp fexp1Valid_exp fexp2
   (choice1 choice2 : Zbool),
  ( n, (beta = 2 × n :> Z)%Z) →
  double_round_div_hyp fexp1 fexp2
   x y,
  y 0 →
  generic_format beta fexp1 x
  generic_format beta fexp1 y
  double_round_eq fexp1 fexp2 choice1 choice2 (x / y).

Section Double_round_div_FLX.

Require Import Fcore_FLX.

Variable prec : Z.
Variable prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLX_double_round_div_hyp :
  (2 × prec prec')%Z
  double_round_div_hyp (FLX_exp prec) (FLX_exp prec').

Theorem double_round_div_FLX :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z) →
  (2 × prec prec')%Z
   x y,
  y 0 →
  FLX_format beta prec xFLX_format beta prec y
  double_round_eq (FLX_exp prec) (FLX_exp prec') choice1 choice2 (x / y).

End Double_round_div_FLX.

Section Double_round_div_FLT.

Require Import Fcore_FLX.
Require Import Fcore_FLT.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FLT_double_round_div_hyp :
  (emin' emin - prec - 2)%Z
  (2 × prec prec')%Z
  double_round_div_hyp (FLT_exp emin prec) (FLT_exp emin' prec').

Theorem double_round_div_FLT :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z) →
  (emin' emin - prec - 2)%Z
  (2 × prec prec')%Z
   x y,
  y 0 →
  FLT_format beta emin prec xFLT_format beta emin prec y
  double_round_eq (FLT_exp emin prec) (FLT_exp emin' prec')
                  choice1 choice2 (x / y).

End Double_round_div_FLT.

Section Double_round_div_FTZ.

Require Import Fcore_FLX.
Require Import Fcore_FTZ.

Variable emin prec : Z.
Variable emin' prec' : Z.

Context { prec_gt_0_ : Prec_gt_0 prec }.
Context { prec_gt_0_' : Prec_gt_0 prec' }.

Lemma FTZ_double_round_div_hyp :
  (emin' + prec' emin - 1)%Z
  (2 × prec prec')%Z
  double_round_div_hyp (FTZ_exp emin prec) (FTZ_exp emin' prec').

Theorem double_round_div_FTZ :
   choice1 choice2,
  ( n, (beta = 2 × n :> Z)%Z) →
  (emin' + prec' emin - 1)%Z
  (2 × prec prec')%Z
   x y,
  y 0 →
  FTZ_format beta emin prec xFTZ_format beta emin prec y
  double_round_eq (FTZ_exp emin prec) (FTZ_exp emin' prec')
                  choice1 choice2 (x / y).

End Double_round_div_FTZ.

End Double_round_div.

End Double_round.