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

Copyright (C) 2010-2013 Sylvie Boldo
#<br />#
Copyright (C) 2010-2013 Guillaume Melquiond

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 Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.

Section Fcalc_div.

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

(** 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.
*)

Definition Fdiv_core prec m1 e1 m2 e2 :=
  let d1 := Zdigits beta m1 in
  let d2 := Zdigits beta m2 in
  let e := (e1 - e2)%Z in
  let (m, e') :=
    match (d2 + prec - d1)%Z with
    | Zpos p => (m1 * Zpower_pos beta p, e + Zneg p)%Z
    | _ => (m1, e)
    end in
  let '(q, r) :=  Zdiv_eucl m m2 in
  (q, e', new_location m2 r loc_Exact).

Theorem Fdiv_core_correct :
  forall prec m1 e1 m2 e2,
  (0 < prec)%Z ->
  (0 < m1)%Z -> (0 < m2)%Z ->
  let '(m, e, l) := Fdiv_core prec m1 e1 m2 e2 in
  (prec <= Zdigits beta m)%Z /\
  inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.
Proof.
(* Goal: forall (prec m1 e1 m2 e2 : Z) (_ : Z.lt Z0 prec) (_ : Z.lt Z0 m1) (_ : Z.lt Z0 m2), let 'pair (pair m e as p) l := Fdiv_core prec m1 e1 m2 e2 in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
intros prec m1 e1 m2 e2 Hprec Hm1 Hm2.
(* Goal: let 'pair (pair m e as p) l := Fdiv_core prec m1 e1 m2 e2 in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
unfold Fdiv_core.
(* Goal: let 'pair (pair m e as p) l := let (m, e') := match Z.sub (Z.add (Zdigits beta m2) prec) (Zdigits beta m1) with | Z0 => @pair Z Z m1 (Z.sub e1 e2) | Zpos p => @pair Z Z (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.sub e1 e2) (Zneg p)) | Zneg p => @pair Z Z m1 (Z.sub e1 e2) end in let 'pair q r := Z.div_eucl m m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
set (d1 := Zdigits beta m1).
(* Goal: let 'pair (pair m e as p) l := let (m, e') := match Z.sub (Z.add (Zdigits beta m2) prec) d1 with | Z0 => @pair Z Z m1 (Z.sub e1 e2) | Zpos p => @pair Z Z (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.sub e1 e2) (Zneg p)) | Zneg p => @pair Z Z m1 (Z.sub e1 e2) end in let 'pair q r := Z.div_eucl m m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
set (d2 := Zdigits beta m2).
case_eq
 (match (d2 + prec - d1)%Z with
  | Zpos p => ((m1 * Zpower_pos beta p)%Z, (e1 - e2 + Zneg p)%Z)
  | _ => (m1, (e1 - e2)%Z)
  end).
(* Goal: forall (z z0 : Z) (_ : @eq (prod Z Z) match Z.sub (Z.add d2 prec) d1 with | Z0 => @pair Z Z m1 (Z.sub e1 e2) | Zpos p => @pair Z Z (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.sub e1 e2) (Zneg p)) | Zneg p => @pair Z Z m1 (Z.sub e1 e2) end (@pair Z Z z z0)), let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl z m2 in @pair (prod Z Z) location (@pair Z Z q z0) (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
intros m' e' Hme.
(* . the shifted mantissa m' has enough digits *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
assert (Hs: F2R (Float beta m' (e' + e2)) = F2R (Float beta m1 e1) /\ (0 < m')%Z /\ (d2 + prec <= Zdigits beta m')%Z).
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 m') (Z.le (Z.add d2 prec) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
replace (d2 + prec)%Z with (d2 + prec - d1 + d1)%Z by ring.
destruct (d2 + prec - d1)%Z as [|p|p] ;
  unfold d1 ;
  inversion Hme.
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add Z0 (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.add (Z.sub e1 e2) (Zneg p)) e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
ring_simplify (e1 - e2 + e2)%Z.
(* Goal: and (@eq R (@F2R beta (Float beta m' e1)) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add Z0 (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.add (Z.sub e1 e2) (Zneg p)) e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
repeat split.
(* Goal: Z.lt Z0 m' *)
(* Goal: Z.le (Z.add Z0 (Zdigits beta m')) (Zdigits beta m') *)
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.add (Z.sub e1 e2) (Zneg p)) e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
now rewrite <- H0.
(* Goal: Z.le (Z.add (Zdigits beta m1) (Zpos p)) (Z.add (Zdigits beta m1) (Zpos p)) *)
(* Goal: not (@eq Z m1 Z0) *)
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply Zle_refl.
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.add (Z.sub e1 e2) (Zneg p)) e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
replace (e1 - e2 + Zneg p + e2)%Z with (e1 - Zpos p)%Z by (unfold Zminus ; simpl ; ring).
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.sub e1 (Zpos p)))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
fold (Zpower beta (Zpos p)).
(* Goal: and (Z.le prec (Zdigits beta q)) (inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact)) *)
split.
(* Goal: @eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))) (Z.sub e1 (Zpos p)))) (@F2R beta (Float beta m1 e1)) *)
(* Goal: and (Z.lt Z0 (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
pattern (Zpos p) at 1 ; replace (Zpos p) with (e1 - (e1 - Zpos p))%Z by ring.
(* Goal: @eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 (Z.sub e1 (Zpos p))))) (Z.sub e1 (Zpos p)))) (@F2R beta (Float beta m1 e1)) *)
(* Goal: and (Z.lt Z0 (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply sym_eq.
(* Goal: @eq R (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta (Z.mul m1 (Z.pow (radix_val beta) (Z.sub e1 (Z.sub e1 (Zpos p))))) (Z.sub e1 (Zpos p)))) *)
(* Goal: and (Z.lt Z0 (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply F2R_change_exp.
(* Goal: Z.le (Z.sub e1 (Zpos p)) e1 *)
(* Goal: and (Z.lt Z0 (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
assert (0 < Zpos p)%Z by easy.
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
omega.
(* Goal: and (Z.le prec (Zdigits beta q)) (inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact)) *)
split.
(* Goal: Z.lt Z0 (Z.mul m1 (Z.pow (radix_val beta) (Zpos p))) *)
(* Goal: Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply Zmult_lt_0_compat.
(* Goal: Z.lt Z0 m1 *)
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Zpos p)) *)
(* Goal: Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
exact Hm1.
(* Goal: Z.lt Z0 (Z.pow (radix_val beta) (Zpos p)) *)
(* Goal: Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
now apply Zpower_gt_0.
(* Goal: Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow (radix_val beta) (Zpos p)))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
rewrite Zdigits_mult_Zpower.
(* Goal: Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Z.add (Zdigits beta m1) (Zpos p)) *)
(* Goal: not (@eq Z m1 Z0) *)
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
rewrite Zplus_comm.
(* Goal: Z.le (Z.add (Zdigits beta m1) (Zpos p)) (Z.add (Zdigits beta m1) (Zpos p)) *)
(* Goal: not (@eq Z m1 Z0) *)
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply Zle_refl.
(* Goal: not (@eq Z m1 Z0) *)
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply sym_not_eq.
(* Goal: not (@eq Z Z0 m1) *)
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
now apply Zlt_not_eq.
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
easy.
(* Goal: and (Z.le prec (Zdigits beta q)) (inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact)) *)
split.
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add Z0 (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: and (@eq R (@F2R beta (Float beta (Z.mul m1 (Z.pow_pos (radix_val beta) p)) (Z.add (Z.add (Z.sub e1 e2) (Zneg p)) e2))) (@F2R beta (Float beta m1 e1))) (and (Z.lt Z0 (Z.mul m1 (Z.pow_pos (radix_val beta) p))) (Z.le (Z.add (Zpos p) (Zdigits beta m1)) (Zdigits beta (Z.mul m1 (Z.pow_pos (radix_val beta) p))))) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
now ring_simplify (e1 - e2 + e2)%Z.
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
assert (Zneg p < 0)%Z by easy.
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
omega.
(* . *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
destruct Hs as (Hs1, (Hs2, Hs3)).
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
rewrite <- Hs1.
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) l) *)
generalize (Z_div_mod m' m2 (Zlt_gt _ _ Hm2)).
(* Goal: forall _ : let (q, r) := Z.div_eucl m' m2 in and (@eq Z m' (Z.add (Z.mul m2 q) r)) (and (Z.le Z0 r) (Z.lt r m2)), let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) l) *)
destruct (Zdiv_eucl m' m2) as (q, r).
(* Goal: forall _ : and (@eq Z m' (Z.add (Z.mul m2 q) r)) (and (Z.le Z0 r) (Z.lt r m2)), and (Z.le prec (Zdigits beta q)) (inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact)) *)
intros (Hq, Hr).
(* Goal: and (Z.le prec (Zdigits beta q)) (inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact)) *)
split.
(* . the result mantissa q has enough digits *)
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
cut (Zdigits beta m' <= d2 + Zdigits beta q)%Z. omega.
(* Goal: Z.le (Zdigits beta m') (Z.add d2 (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
unfold d2.
(* Goal: @eq Z (Z.mul q m2) (Z.sub m' r) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
rewrite Hq.
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
assert (Hq': (0 < q)%Z).
(* Goal: Z.lt Z0 q *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
apply Zmult_lt_reg_r with (1 := Hm2).
(* Goal: Z.lt (Z.mul Z0 m2) (Z.mul q m2) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
assert (m2 < m')%Z.
(* Goal: Z.lt m2 m' *)
(* Goal: Z.lt (Z.mul Z0 m2) (Z.mul q m2) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
apply lt_Zdigits with beta.
(* Goal: Z.le Z0 m' *)
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
now apply Zlt_le_weak.
(* Goal: Z.lt (Zdigits beta m2) (Zdigits beta m') *)
(* Goal: Z.lt (Z.mul Z0 m2) (Z.mul q m2) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
unfold d2 in Hs3.
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
clear -Hprec Hs3 ; omega.
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
cut (q * m2 = m' - r)%Z. clear -Hr H ; omega.
(* Goal: @eq Z (Z.mul q m2) (Z.sub m' r) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
rewrite Hq.
(* Goal: @eq Z (Z.mul q m2) (Z.sub (Z.add (Z.mul m2 q) r) r) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
ring.
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
apply Zle_trans with (Zdigits beta (m2 + q + m2 * q)).
(* Goal: Z.le (Zdigits beta (Z.add (Z.mul m2 q) r)) (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
apply Zdigits_le.
(* Goal: Z.le Z0 (Z.add (Z.mul m2 q) r) *)
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
rewrite <- Hq.
(* Goal: Z.le Z0 m' *)
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
now apply Zlt_le_weak.
(* Goal: Z.le (Z.add (Z.mul m2 q) r) (Z.add (Z.add m2 q) (Z.mul m2 q)) *)
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
clear -Hr Hq'. omega.
(* Goal: Z.le (Zdigits beta (Z.add (Z.add m2 q) (Z.mul m2 q))) (Z.add (Zdigits beta m2) (Zdigits beta q)) *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
apply Zdigits_mult_strong ; apply Zlt_le_weak.
(* Goal: Z.lt Z0 m2 *)
(* Goal: Z.lt Z0 q *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
now apply Zle_lt_trans with r.
(* Goal: Z.lt Z0 q *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
exact Hq'.
(* . the location is correctly computed *)
(* Goal: inbetween_float beta q e' (Rdiv (@F2R beta (Float beta m' (Z.add e' e2))) (@F2R beta (Float beta m2 e2))) (new_location m2 r loc_Exact) *)
unfold inbetween_float, F2R. simpl.
(* Goal: inbetween (Rmult (Z2R q) (Fcore_Raux.bpow beta e')) (Rmult (Z2R (Z.add q (Zpos xH))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Z2R m') (Fcore_Raux.bpow beta (Z.add e' e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) (new_location m2 r loc_Exact) *)
rewrite bpow_plus, Z2R_plus.
(* Goal: inbetween (Rmult (Z2R q) (Fcore_Raux.bpow beta e')) (Rmult (Rplus (Z2R q) (Z2R (Zpos xH))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Z2R m') (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) (new_location m2 r loc_Exact) *)
rewrite Hq, Z2R_plus, Z2R_mult.
replace ((Z2R m2 * Z2R q + Z2R r) * (bpow e' * bpow e2) / (Z2R m2 * bpow e2))%R
  with ((Z2R q + Z2R r / Z2R m2) * bpow e')%R.
(* Goal: inbetween (Rmult (Z2R q) (Fcore_Raux.bpow beta e')) (Rmult (Rplus (Z2R q) (Z2R (Zpos xH))) (Fcore_Raux.bpow beta e')) (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
apply inbetween_mult_compat.
(* Goal: Rgt (Fcore_Raux.bpow beta e2) (IZR Z0) *)
(* Goal: Rgt (Z2R m2) (IZR Z0) *)
apply bpow_gt_0.
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
destruct (Z_lt_le_dec 1 m2) as [Hm2''|Hm2''].
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
replace (Z2R 1) with (Z2R m2 * /Z2R m2)%R.
(* Goal: Z.le Z0 (Zpos p) *)
(* Goal: and (@eq R (@F2R beta (Float beta m' (Z.add (Z.sub e1 e2) e2))) (@F2R beta (Float beta m' e1))) (and (Z.lt Z0 m') (Z.le (Z.add (Zneg p) (Zdigits beta m')) (Zdigits beta m'))) *)
(* Goal: let 'pair (pair m e as p) l := let 'pair q r := Z.div_eucl m' m2 in @pair (prod Z Z) location (@pair Z Z q e') (new_location m2 r loc_Exact) in and (Z.le prec (Zdigits beta m)) (inbetween_float beta m e (Rdiv (@F2R beta (Float beta m1 e1)) (@F2R beta (Float beta m2 e2))) l) *)
apply new_location_correct ; try easy.
(* Goal: Rlt (IZR Z0) (Rinv (Z2R m2)) *)
(* Goal: inbetween (Rplus (Z2R q) (Rmult (Z2R r) (Rinv (Z2R m2)))) (Rplus (Z2R q) (Rmult (Z2R (Z.add r (Zpos xH))) (Rinv (Z2R m2)))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) loc_Exact *)
(* Goal: @eq R (Rmult (Z2R m2) (Rinv (Z2R m2))) (Z2R (Zpos xH)) *)
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
apply Rinv_0_lt_compat.
(* Goal: Rgt (Z2R m2) (IZR Z0) *)
now apply (Z2R_lt 0).
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Z2R q) (new_location (Zpos xH) Z0 loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
now constructor.
(* Goal: @eq R (Rmult (Z2R m2) (Rinv (Z2R m2))) (Z2R (Zpos xH)) *)
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
apply Rinv_r.
(* Goal: not (@eq R (Z2R m2) (IZR Z0)) *)
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
apply Rgt_not_eq.
(* Goal: Rgt (Z2R m2) (IZR Z0) *)
now apply (Z2R_lt 0).
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
assert (r = 0 /\ m2 = 1)%Z by (clear -Hr Hm2'' ; omega).
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
rewrite (proj1 H), (proj2 H).
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R Z0) (Z2R (Zpos xH)))) (new_location (Zpos xH) Z0 loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
unfold Rdiv.
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rmult (Z2R Z0) (Rinv (Z2R (Zpos xH))))) (new_location (Zpos xH) Z0 loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
rewrite Rmult_0_l, Rplus_0_r.
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Z2R q) (new_location (Zpos xH) Z0 loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
now constructor.
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
field.
(* Goal: not (@eq R (Z2R m2) (IZR Z0)) *)
(* Goal: inbetween (Z2R q) (Rplus (Z2R q) (Z2R (Zpos xH))) (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (new_location m2 r loc_Exact) *)
(* Goal: @eq R (Rmult (Rplus (Z2R q) (Rdiv (Z2R r) (Z2R m2))) (Fcore_Raux.bpow beta e')) (Rdiv (Rmult (Rplus (Rmult (Z2R m2) (Z2R q)) (Z2R r)) (Rmult (Fcore_Raux.bpow beta e') (Fcore_Raux.bpow beta e2))) (Rmult (Z2R m2) (Fcore_Raux.bpow beta e2))) *)
split ; apply Rgt_not_eq.
(* Goal: Rgt (Fcore_Raux.bpow beta e2) (IZR Z0) *)
(* Goal: Rgt (Z2R m2) (IZR Z0) *)
apply bpow_gt_0.
(* Goal: Rgt (Z2R m2) (IZR Z0) *)
now apply (Z2R_lt 0).
Qed.

End Fcalc_div.
