Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Helper function and theorem for computing the rounded quotient of two floating-point numbers.

Require Import Raux Defs Generic_fmt Float_prop Digits Bracket.

Set Implicit Arguments.
Set Strongly Strict Implicit.

Section Fcalc_div.

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

Variable fexp : Z -> Z.

Computes a mantissa of precision p, the corresponding exponent, and the position with respect to the real quotient of the input floating-point numbers.

The algorithm performs the following steps:

Shift dividend mantissa so that it has at least p2 + p digits.
Perform the Euclidean division.
Compute the position according to the division remainder.

Complexity is fine as long as p1 <= 2p and p2 <= p.

Lemma mag_div_F2R :
  forall m1 e1 m2 e2,
  (0 < m1)%Z -> (0 < m2)%Z ->
  let e := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
  (e <= mag beta (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) <= e + 1)%Z.beta:radix
fexp:Z -> Z
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
(0 < m2)%Z ->
let e :=
  (Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z in
(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z
Proof.beta:radix
fexp:Z -> Z
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
(0 < m2)%Z ->
let e :=
  (Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z in
(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z
intros m1 e1 m2 e2 Hm1 Hm2.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let e :=
  (Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z in
(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z
rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let e :=
  (mag beta (F2R {| Fnum := m1; Fexp := e1 |}) -
   (Zdigits beta m2 + e2))%Z in
(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z
rewrite <- (mag_F2R_Zdigits beta m2 e2) by now apply Zgt_not_eq.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let e :=
  (mag beta (F2R {| Fnum := m1; Fexp := e1 |}) -
   mag beta (F2R {| Fnum := m2; Fexp := e2 |}))%Z in
(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z
apply mag_div.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
F2R {| Fnum := m1; Fexp := e1 |} <> 0%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
F2R {| Fnum := m2; Fexp := e2 |} <> 0%R
now apply F2R_neq_0, Zgt_not_eq.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
F2R {| Fnum := m2; Fexp := e2 |} <> 0%R
now apply F2R_neq_0, Zgt_not_eq.
Qed.

Definition Fdiv_core m1 e1 m2 e2 e :=
  let (m1', m2') :=
    if Zle_bool e (e1 - e2)%Z
    then (m1 * Zpower beta (e1 - e2 - e), m2)%Z
    else (m1, m2 * Zpower beta (e - (e1 - e2)))%Z in
  let '(q, r) :=  Z.div_eucl m1' m2' in
  (q, new_location m2' r loc_Exact).

Theorem Fdiv_core_correct :
  forall m1 e1 m2 e2 e,
  (0 < m1)%Z -> (0 < m2)%Z ->
  let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
  inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.beta:radix
fexp:Z -> Z
forall m1 e1 m2 e2 e : Z,
(0 < m1)%Z ->
(0 < m2)%Z ->
let
'(m, l) := Fdiv_core m1 e1 m2 e2 e in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
Proof.beta:radix
fexp:Z -> Z
forall m1 e1 m2 e2 e : Z,
(0 < m1)%Z ->
(0 < m2)%Z ->
let
'(m, l) := Fdiv_core m1 e1 m2 e2 e in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
intros m1 e1 m2 e2 e Hm1 Hm2.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let
'(m, l) := Fdiv_core m1 e1 m2 e2 e in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
unfold Fdiv_core.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let
'(m, l) :=
 let (m1', m2') :=
   if (e <=? e1 - e2)%Z
   then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
   else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z) in
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
match goal with |- context [if ?b then ?b1 else ?b2] => set (m12 := if b then b1 else b2) end.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
let
'(m, l) :=
 let (m1', m2') := m12 in
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
case_eq m12 ; intros m1' m2' Hm.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
let
'(m, l) :=
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z) as [Hf Hm2'].beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
let
'(m, l) :=
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
{beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z unfold F2R, Zminus ; simpl.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
(IZR m1 * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR m2' * bpow e)%R /\ (0 < m2')%Z
  destruct (Zle_bool e (e1 - e2)) eqn:He' ; injection Hm ; intros ; subst.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <=? e1 - e2)%Z = true
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR (m1 * beta ^ (e1 - e2 - e)) / IZR m2' * bpow e)%R /\
(0 < m2')%Z
beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e <=? e1 - e2)%Z = false
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR (m2 * beta ^ (e - (e1 - e2))) * bpow e)%R /\
(0 < m2 * beta ^ (e - (e1 - e2)))%Z
  -beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <=? e1 - e2)%Z = true
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR (m1 * beta ^ (e1 - e2 - e)) / IZR m2' * bpow e)%R /\
(0 < m2')%Z split ; try easy.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <=? e1 - e2)%Z = true
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR (m1 * beta ^ (e1 - e2 - e)) / IZR m2' * bpow e)%R
    apply Zle_bool_imp_le in He'.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <= e1 - e2)%Z
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR (m1 * beta ^ (e1 - e2 - e)) / IZR m2' * bpow e)%R
    rewrite mult_IZR, IZR_Zpower by omega.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <= e1 - e2)%Z
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR m1 * bpow (e1 - e2 - e) / IZR m2' * bpow e)%R
    unfold Zminus ; rewrite 2!bpow_plus, 2!bpow_opp.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <= e1 - e2)%Z
(IZR m1 * bpow e1 / (IZR m2' * bpow e2))%R =
(IZR m1 * (bpow e1 * / bpow e2 * / bpow e) / IZR m2' *
 bpow e)%R
    field.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <= e1 - e2)%Z
bpow e <> 0%R /\ bpow e2 <> 0%R /\ IZR m2' <> 0%R
    repeat split ; try apply Rgt_not_eq, bpow_gt_0.beta:radix
fexp:Z -> Z
m1, e1, e2, e:Z
Hm1:(0 < m1)%Z
m2':Z
m12:=((m1 * beta ^ (e1 - e2 - e))%Z, m2'):(Z * Z)%type
Hm:m12 = ((m1 * beta ^ (e1 - e2 - e))%Z, m2')
Hm2:(0 < m2')%Z
He':(e <= e1 - e2)%Z
IZR m2' <> 0%R
    now apply IZR_neq, Zgt_not_eq.
  -beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e <=? e1 - e2)%Z = false
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR (m2 * beta ^ (e - (e1 - e2))) * bpow e)%R /\
(0 < m2 * beta ^ (e - (e1 - e2)))%Z apply Z.leb_gt in He'.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR (m2 * beta ^ (e - (e1 - e2))) * bpow e)%R /\
(0 < m2 * beta ^ (e - (e1 - e2)))%Z
    split ; cycle 1.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(0 < m2 * beta ^ (e - (e1 - e2)))%Z
beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR (m2 * beta ^ (e - (e1 - e2))) * bpow e)%R
    {beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(0 < m2 * beta ^ (e - (e1 - e2)))%Z apply Z.mul_pos_pos with (1 := Hm2).beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(0 < beta ^ (e - (e1 - e2)))%Z
      apply Zpower_gt_0 ; omega. }beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / IZR (m2 * beta ^ (e - (e1 - e2))) * bpow e)%R
    rewrite mult_IZR, IZR_Zpower by omega.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' / (IZR m2 * bpow (e - (e1 - e2))) * bpow e)%R
    unfold Zminus ; rewrite bpow_plus, bpow_opp, bpow_plus, bpow_opp.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
(IZR m1' * bpow e1 / (IZR m2 * bpow e2))%R =
(IZR m1' /
 (IZR m2 * (bpow e * / (bpow e1 * / bpow e2))) *
 bpow e)%R
    field.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
bpow e2 <> 0%R /\
bpow e1 <> 0%R /\ bpow e <> 0%R /\ IZR m2 <> 0%R
    repeat split ; try apply Rgt_not_eq, bpow_gt_0.beta:radix
fexp:Z -> Z
e1, m2, e2, e, m1':Z
m12:=(m1', (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
Hm:m12 = (m1', (m2 * beta ^ (e - (e1 - e2)))%Z)
Hm1:(0 < m1')%Z
Hm2:(0 < m2)%Z
He':(e1 - e2 < e)%Z
IZR m2 <> 0%R
    now apply IZR_neq, Zgt_not_eq. }beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
m12:=if (e <=? e1 - e2)%Z
then ((m1 * beta ^ (e1 - e2 - e))%Z, m2)
else (m1, (m2 * beta ^ (e - (e1 - e2)))%Z):(Z * Z)%type
m1', m2':Z
Hm:m12 = (m1', m2')
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
let
'(m, l) :=
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
clearbody m12 ; clear Hm Hm1 Hm2.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
let
'(m, l) :=
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
generalize (Z_div_mod m1' m2' (Z.lt_gt _ _ Hm2')).beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
(let (q, r) := Z.div_eucl m1' m2' in
 m1' = (m2' * q + r)%Z /\ (0 <= r < m2')%Z) ->
let
'(m, l) :=
 let
 '(q, r) := Z.div_eucl m1' m2' in
  (q, new_location m2' r SpecFloatCopy.loc_Exact) in
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
destruct (Z.div_eucl m1' m2') as (q, r).beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
m1' = (m2' * q + r)%Z /\ (0 <= r < m2')%Z ->
inbetween_float beta q e
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
  (new_location m2' r SpecFloatCopy.loc_Exact)
intros (Hq, Hr).beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween_float beta q e
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
  (new_location m2' r SpecFloatCopy.loc_Exact)
rewrite Hf.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween_float beta q e (IZR m1' / IZR m2' * bpow e)
  (new_location m2' r SpecFloatCopy.loc_Exact)
unfold inbetween_float, F2R.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween
  (IZR (Fnum {| Fnum := q; Fexp := e |}) *
   bpow (Fexp {| Fnum := q; Fexp := e |}))
  (IZR (Fnum {| Fnum := q + 1; Fexp := e |}) *
   bpow (Fexp {| Fnum := q + 1; Fexp := e |}))
  (IZR m1' / IZR m2' * bpow e)
  (new_location m2' r SpecFloatCopy.loc_Exact) simpl.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween (IZR q * bpow e) (IZR (q + 1) * bpow e)
  (IZR m1' / IZR m2' * bpow e)
  (new_location m2' r SpecFloatCopy.loc_Exact)
rewrite Hq, 2!plus_IZR, mult_IZR.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween (IZR q * bpow e) ((IZR q + 1) * bpow e)
  ((IZR m2' * IZR q + IZR r) / IZR m2' * bpow e)
  (new_location m2' r SpecFloatCopy.loc_Exact)
apply inbetween_mult_compat.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
(0 < bpow e)%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact)
  apply bpow_gt_0.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact)
destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact)
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(m2' <= 1)%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact)
-beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact) replace 1%R with (IZR m2' * /IZR m2')%R.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q) (IZR q + IZR m2' * / IZR m2')
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact)
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  apply new_location_correct ; try easy.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(0 < / IZR m2')%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q + IZR r * / IZR m2')
  (IZR q + IZR (r + 1) * / IZR m2')
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  apply Rinv_0_lt_compat.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(0 < IZR m2')%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q + IZR r * / IZR m2')
  (IZR q + IZR (r + 1) * / IZR m2')
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  now apply IZR_lt.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
inbetween (IZR q + IZR r * / IZR m2')
  (IZR q + IZR (r + 1) * / IZR m2')
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  SpecFloatCopy.loc_Exact
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  constructor.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
((IZR m2' * IZR q + IZR r) / IZR m2')%R =
(IZR q + IZR r * / IZR m2')%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  field.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
IZR m2' <> 0%R
beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  now apply IZR_neq, Zgt_not_eq.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
(IZR m2' * / IZR m2')%R = 1%R
  field.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(1 < m2')%Z
IZR m2' <> 0%R
  now apply IZR_neq, Zgt_not_eq.
-beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1', m2':Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / IZR m2' * bpow e)%R
Hm2':(0 < m2')%Z
q, r:Z
Hq:m1' = (m2' * q + r)%Z
Hr:(0 <= r < m2')%Z
Hm2'':(m2' <= 1)%Z
inbetween (IZR q) (IZR q + 1)
  ((IZR m2' * IZR q + IZR r) / IZR m2')
  (new_location m2' r SpecFloatCopy.loc_Exact) assert (r = 0 /\ m2' = 1)%Z as [-> ->] by (clear -Hr Hm2'' ; omega).beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1':Z
Hm2':(0 < 1)%Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / 1 * bpow e)%R
q:Z
Hm2'':(1 <= 1)%Z
Hq:m1' = (1 * q + 0)%Z
Hr:(0 <= 0 < 1)%Z
inbetween (IZR q) (IZR q + 1) ((1 * IZR q + 0) / 1)
  (new_location 1 0 SpecFloatCopy.loc_Exact)
  unfold Rdiv.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1':Z
Hm2':(0 < 1)%Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / 1 * bpow e)%R
q:Z
Hm2'':(1 <= 1)%Z
Hq:m1' = (1 * q + 0)%Z
Hr:(0 <= 0 < 1)%Z
inbetween (IZR q) (IZR q + 1) ((1 * IZR q + 0) * / 1)
  (new_location 1 0 SpecFloatCopy.loc_Exact)
  rewrite Rmult_1_l, Rplus_0_r, Rinv_1, Rmult_1_r.beta:radix
fexp:Z -> Z
m1, e1, m2, e2, e:Z
m12:(Z * Z)%type
m1':Z
Hm2':(0 < 1)%Z
Hf:(F2R {| Fnum := m1; Fexp := e1 |} /
 F2R {| Fnum := m2; Fexp := e2 |})%R =
(IZR m1' / 1 * bpow e)%R
q:Z
Hm2'':(1 <= 1)%Z
Hq:m1' = (1 * q + 0)%Z
Hr:(0 <= 0 < 1)%Z
inbetween (IZR q) (IZR q + 1) (IZR q)
  (new_location 1 0 SpecFloatCopy.loc_Exact)
  now constructor.
Qed.

Definition Fdiv (x y : float beta) :=
  let (m1, e1) := x in
  let (m2, e2) := y in
  let e' := ((Zdigits beta m1 + e1) - (Zdigits beta m2 + e2))%Z in
  let e := Z.min (Z.min (fexp e') (fexp (e' + 1))) (e1 - e2) in
  let '(m, l) := Fdiv_core m1 e1 m2 e2 e in
  (m, e, l).

Theorem Fdiv_correct :
  forall x y,
  (0 < F2R x)%R -> (0 < F2R y)%R ->
  let '(m, e, l) := Fdiv x y in
  (e <= cexp beta fexp (F2R x / F2R y))%Z /\
  inbetween_float beta m e (F2R x / F2R y) l.beta:radix
fexp:Z -> Z
forall x y : float beta,
(0 < F2R x)%R ->
(0 < F2R y)%R ->
let
'(m, e, l) := Fdiv x y in
 (e <= cexp beta fexp (F2R x / F2R y))%Z /\
 inbetween_float beta m e (F2R x / F2R y) l
Proof.beta:radix
fexp:Z -> Z
forall x y : float beta,
(0 < F2R x)%R ->
(0 < F2R y)%R ->
let
'(m, e, l) := Fdiv x y in
 (e <= cexp beta fexp (F2R x / F2R y))%Z /\
 inbetween_float beta m e (F2R x / F2R y) l
intros [m1 e1] [m2 e2] Hm1 Hm2.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < F2R {| Fnum := m1; Fexp := e1 |})%R
Hm2:(0 < F2R {| Fnum := m2; Fexp := e2 |})%R
let
'(m, e, l) :=
 Fdiv {| Fnum := m1; Fexp := e1 |}
   {| Fnum := m2; Fexp := e2 |} in
 (e <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
apply gt_0_F2R in Hm1.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < F2R {| Fnum := m2; Fexp := e2 |})%R
let
'(m, e, l) :=
 Fdiv {| Fnum := m1; Fexp := e1 |}
   {| Fnum := m2; Fexp := e2 |} in
 (e <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
apply gt_0_F2R in Hm2.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let
'(m, e, l) :=
 Fdiv {| Fnum := m1; Fexp := e1 |}
   {| Fnum := m2; Fexp := e2 |} in
 (e <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
unfold Fdiv.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
let
'(m, e, l) :=
 let
 '(m, l) :=
  Fdiv_core m1 e1 m2 e2
    (Z.min
       (Z.min
          (fexp
             (Zdigits beta m1 + e1 -
              (Zdigits beta m2 + e2)))
          (fexp
             (Zdigits beta m1 + e1 -
              (Zdigits beta m2 + e2) + 1))) (e1 - e2))
  in
  (m,
  Z.min
    (Z.min
       (fexp
          (Zdigits beta m1 + e1 -
           (Zdigits beta m2 + e2)))
       (fexp
          (Zdigits beta m1 + e1 -
           (Zdigits beta m2 + e2) + 1))) (e1 - e2), l)
 in
 (e <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
generalize (mag_div_F2R m1 e1 m2 e2 Hm1 Hm2).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
(let e :=
   (Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z
   in
 (e <=
  mag beta
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}) <= e + 1)%Z) ->
let
'(m, e, l) :=
 let
 '(m, l) :=
  Fdiv_core m1 e1 m2 e2
    (Z.min
       (Z.min
          (fexp
             (Zdigits beta m1 + e1 -
              (Zdigits beta m2 + e2)))
          (fexp
             (Zdigits beta m1 + e1 -
              (Zdigits beta m2 + e2) + 1))) (e1 - e2))
  in
  (m,
  Z.min
    (Z.min
       (fexp
          (Zdigits beta m1 + e1 -
           (Zdigits beta m2 + e2)))
       (fexp
          (Zdigits beta m1 + e1 -
           (Zdigits beta m2 + e2) + 1))) (e1 - e2), l)
 in
 (e <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
set (e := Zminus _ _).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
(let e0 := e in
 (e0 <=
  mag beta
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}) <= e0 + 1)%Z) ->
let
'(m, e0, l) :=
 let
 '(m, l) :=
  Fdiv_core m1 e1 m2 e2
    (Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2))
  in
  (m, Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2),
  l) in
 (e0 <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e0
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
set (e' := Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2)).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
(let e0 := e in
 (e0 <=
  mag beta
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}) <= e0 + 1)%Z) ->
let
'(m, e0, l) :=
 let '(m, l) := Fdiv_core m1 e1 m2 e2 e' in (m, e', l)
 in
 (e0 <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e0
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
intros [H1 H2].beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
let
'(m, e0, l) :=
 let '(m, l) := Fdiv_core m1 e1 m2 e2 e' in (m, e', l)
 in
 (e0 <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e0
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
generalize (Fdiv_core_correct m1 e1 m2 e2 e' Hm1 Hm2).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
(let
 '(m, l) := Fdiv_core m1 e1 m2 e2 e' in
  inbetween_float beta m e'
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}) l) ->
let
'(m, e0, l) :=
 let '(m, l) := Fdiv_core m1 e1 m2 e2 e' in (m, e', l)
 in
 (e0 <=
  cexp beta fexp
    (F2R {| Fnum := m1; Fexp := e1 |} /
     F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
 inbetween_float beta m e0
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) l
destruct Fdiv_core as [m' l].beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
inbetween_float beta m' e'
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |}) l ->
(e' <=
 cexp beta fexp
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z /\
inbetween_float beta m' e'
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |}) l
apply conj.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
(e' <=
 cexp beta fexp
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
apply Z.le_trans with (1 := Z.le_min_l _ _).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
(Z.min (fexp e) (fexp (e + 1)) <=
 cexp beta fexp
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
unfold cexp.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
(Z.min (fexp e) (fexp (e + 1)) <=
 fexp
   (mag beta
      (F2R {| Fnum := m1; Fexp := e1 |} /
       F2R {| Fnum := m2; Fexp := e2 |})))%Z
destruct (Zle_lt_or_eq _ _ H1) as [H|H].beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:(e <
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
(Z.min (fexp e) (fexp (e + 1)) <=
 fexp
   (mag beta
      (F2R {| Fnum := m1; Fexp := e1 |} /
       F2R {| Fnum := m2; Fexp := e2 |})))%Z
beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:e =
mag beta
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
(Z.min (fexp e) (fexp (e + 1)) <=
 fexp
   (mag beta
      (F2R {| Fnum := m1; Fexp := e1 |} /
       F2R {| Fnum := m2; Fexp := e2 |})))%Z
-beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:(e <
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
(Z.min (fexp e) (fexp (e + 1)) <=
 fexp
   (mag beta
      (F2R {| Fnum := m1; Fexp := e1 |} /
       F2R {| Fnum := m2; Fexp := e2 |})))%Z replace (fexp (mag _ _)) with (fexp (e + 1)).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:(e <
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
(Z.min (fexp e) (fexp (e + 1)) <= fexp (e + 1))%Z
beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:(e <
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
fexp (e + 1) =
fexp
  (mag beta
     (F2R {| Fnum := m1; Fexp := e1 |} /
      F2R {| Fnum := m2; Fexp := e2 |}))
  apply Z.le_min_r.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:(e <
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
fexp (e + 1) =
fexp
  (mag beta
     (F2R {| Fnum := m1; Fexp := e1 |} /
      F2R {| Fnum := m2; Fexp := e2 |}))
  clear -H1 H2 H ; apply f_equal ; omega.
-beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:e =
mag beta
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
(Z.min (fexp e) (fexp (e + 1)) <=
 fexp
   (mag beta
      (F2R {| Fnum := m1; Fexp := e1 |} /
       F2R {| Fnum := m2; Fexp := e2 |})))%Z replace (fexp (mag _ _)) with (fexp e).beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:e =
mag beta
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
(Z.min (fexp e) (fexp (e + 1)) <= fexp e)%Z
beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:e =
mag beta
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
fexp e =
fexp
  (mag beta
     (F2R {| Fnum := m1; Fexp := e1 |} /
      F2R {| Fnum := m2; Fexp := e2 |}))
  apply Z.le_min_l.beta:radix
fexp:Z -> Z
m1, e1, m2, e2:Z
Hm1:(0 < m1)%Z
Hm2:(0 < m2)%Z
e:=(Zdigits beta m1 + e1 - (Zdigits beta m2 + e2))%Z:Z
e':=Z.min (Z.min (fexp e) (fexp (e + 1))) (e1 - e2):Z
H1:(e <=
 mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}))%Z
H2:(mag beta
   (F2R {| Fnum := m1; Fexp := e1 |} /
    F2R {| Fnum := m2; Fexp := e2 |}) <= 
 e + 1)%Z
m':Z
l:SpecFloatCopy.location
H:e =
mag beta
  (F2R {| Fnum := m1; Fexp := e1 |} /
   F2R {| Fnum := m2; Fexp := e2 |})
fexp e =
fexp
  (mag beta
     (F2R {| Fnum := m1; Fexp := e1 |} /
      F2R {| Fnum := m2; Fexp := e2 |}))
  clear -H1 H2 H ; apply f_equal ; omega.
Qed.

End Fcalc_div.