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.

Basic properties of floating-point formats: lemmas about mantissa, exponent...

Require Import Raux Defs Digits.

Section Float_prop.

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

Theorem Rcompare_F2R :
  forall e m1 m2 : Z,
  Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Z.compare m1 m2.beta:radix
forall e m1 m2 : Z,
Rcompare (F2R {| Fnum := m1; Fexp := e |})
  (F2R {| Fnum := m2; Fexp := e |}) = (m1 ?= m2)%Z
Proof.beta:radix
forall e m1 m2 : Z,
Rcompare (F2R {| Fnum := m1; Fexp := e |})
  (F2R {| Fnum := m2; Fexp := e |}) = (m1 ?= m2)%Z
intros e m1 m2.beta:radix
e, m1, m2:Z
Rcompare (F2R {| Fnum := m1; Fexp := e |})
  (F2R {| Fnum := m2; Fexp := e |}) = (m1 ?= m2)%Z
unfold F2R.beta:radix
e, m1, m2:Z
Rcompare
  (IZR (Fnum {| Fnum := m1; Fexp := e |}) *
   bpow (Fexp {| Fnum := m1; Fexp := e |}))
  (IZR (Fnum {| Fnum := m2; Fexp := e |}) *
   bpow (Fexp {| Fnum := m2; Fexp := e |})) =
(m1 ?= m2)%Z simpl.beta:radix
e, m1, m2:Z
Rcompare (IZR m1 * bpow e) (IZR m2 * bpow e) =
(m1 ?= m2)%Z
rewrite Rcompare_mult_r.beta:radix
e, m1, m2:Z
Rcompare (IZR m1) (IZR m2) = (m1 ?= m2)%Z
beta:radix
e, m1, m2:Z
(0 < bpow e)%R
apply Rcompare_IZR.beta:radix
e, m1, m2:Z
(0 < bpow e)%R
apply bpow_gt_0.
Qed.

Basic facts

Theorem le_F2R :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
  (m1 <= m2)%Z.beta:radix
forall e m1 m2 : Z,
(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R -> (m1 <= m2)%Z
Proof.beta:radix
forall e m1 m2 : Z,
(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R -> (m1 <= m2)%Z
intros e m1 m2 H.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
(m1 <= m2)%Z
apply le_IZR.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 <= IZR m2)%R
apply Rmult_le_reg_r with (bpow e).beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
(0 < bpow e)%R
beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 * bpow e <= IZR m2 * bpow e)%R
apply bpow_gt_0.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 * bpow e <= IZR m2 * bpow e)%R
exact H.
Qed.

Theorem F2R_le :
  forall m1 m2 e : Z,
  (m1 <= m2)%Z ->
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.beta:radix
forall m1 m2 e : Z,
(m1 <= m2)%Z ->
(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
Proof.beta:radix
forall m1 m2 e : Z,
(m1 <= m2)%Z ->
(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
intros m1 m2 e H.beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(F2R {| Fnum := m1; Fexp := e |} <=
 F2R {| Fnum := m2; Fexp := e |})%R
unfold F2R.beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(IZR (Fnum {| Fnum := m1; Fexp := e |}) *
 bpow (Fexp {| Fnum := m1; Fexp := e |}) <=
 IZR (Fnum {| Fnum := m2; Fexp := e |}) *
 bpow (Fexp {| Fnum := m2; Fexp := e |}))%R simpl.beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(IZR m1 * bpow e <= IZR m2 * bpow e)%R
apply Rmult_le_compat_r.beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(0 <= bpow e)%R
beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(IZR m1 <= IZR m2)%R
apply bpow_ge_0.beta:radix
m1, m2, e:Z
H:(m1 <= m2)%Z
(IZR m1 <= IZR m2)%R
now apply IZR_le.
Qed.

Theorem lt_F2R :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
  (m1 < m2)%Z.beta:radix
forall e m1 m2 : Z,
(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R -> (m1 < m2)%Z
Proof.beta:radix
forall e m1 m2 : Z,
(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R -> (m1 < m2)%Z
intros e m1 m2 H.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
(m1 < m2)%Z
apply lt_IZR.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 < IZR m2)%R
apply Rmult_lt_reg_r with (bpow e).beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
(0 < bpow e)%R
beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 * bpow e < IZR m2 * bpow e)%R
apply bpow_gt_0.beta:radix
e, m1, m2:Z
H:(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
(IZR m1 * bpow e < IZR m2 * bpow e)%R
exact H.
Qed.

Theorem F2R_lt :
  forall e m1 m2 : Z,
  (m1 < m2)%Z ->
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.beta:radix
forall e m1 m2 : Z,
(m1 < m2)%Z ->
(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
Proof.beta:radix
forall e m1 m2 : Z,
(m1 < m2)%Z ->
(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
intros e m1 m2 H.beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(F2R {| Fnum := m1; Fexp := e |} <
 F2R {| Fnum := m2; Fexp := e |})%R
unfold F2R.beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(IZR (Fnum {| Fnum := m1; Fexp := e |}) *
 bpow (Fexp {| Fnum := m1; Fexp := e |}) <
 IZR (Fnum {| Fnum := m2; Fexp := e |}) *
 bpow (Fexp {| Fnum := m2; Fexp := e |}))%R simpl.beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(IZR m1 * bpow e < IZR m2 * bpow e)%R
apply Rmult_lt_compat_r.beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(0 < bpow e)%R
beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(IZR m1 < IZR m2)%R
apply bpow_gt_0.beta:radix
e, m1, m2:Z
H:(m1 < m2)%Z
(IZR m1 < IZR m2)%R
now apply IZR_lt.
Qed.

Theorem F2R_eq :
  forall e m1 m2 : Z,
  (m1 = m2)%Z ->
  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.beta:radix
forall e m1 m2 : Z,
m1 = m2 ->
F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |}
Proof.beta:radix
forall e m1 m2 : Z,
m1 = m2 ->
F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |}
intros e m1 m2 H.beta:radix
e, m1, m2:Z
H:m1 = m2
F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |}
now apply (f_equal (fun m => F2R (Float beta m e))).
Qed.

Theorem eq_F2R :
  forall e m1 m2 : Z,
  F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
  m1 = m2.beta:radix
forall e m1 m2 : Z,
F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |} -> m1 = m2
Proof.beta:radix
forall e m1 m2 : Z,
F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |} -> m1 = m2
intros e m1 m2 H.beta:radix
e, m1, m2:Z
H:F2R {| Fnum := m1; Fexp := e |} =
F2R {| Fnum := m2; Fexp := e |}
m1 = m2
apply Zle_antisym ;
  apply le_F2R with e ;
  rewrite H ;
  apply Rle_refl.
Qed.

Theorem F2R_Zabs:
  forall m e : Z,
   F2R (Float beta (Z.abs m) e) = Rabs (F2R (Float beta m e)).beta:radix
forall m e : Z,
F2R {| Fnum := Z.abs m; Fexp := e |} =
Rabs (F2R {| Fnum := m; Fexp := e |})
Proof.beta:radix
forall m e : Z,
F2R {| Fnum := Z.abs m; Fexp := e |} =
Rabs (F2R {| Fnum := m; Fexp := e |})
intros m e.beta:radix
m, e:Z
F2R {| Fnum := Z.abs m; Fexp := e |} =
Rabs (F2R {| Fnum := m; Fexp := e |})
unfold F2R.beta:radix
m, e:Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) *
 bpow (Fexp {| Fnum := Z.abs m; Fexp := e |}))%R =
Rabs
  (IZR (Fnum {| Fnum := m; Fexp := e |}) *
   bpow (Fexp {| Fnum := m; Fexp := e |}))
rewrite Rabs_mult.beta:radix
m, e:Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) *
 bpow (Fexp {| Fnum := Z.abs m; Fexp := e |}))%R =
(Rabs (IZR (Fnum {| Fnum := m; Fexp := e |})) *
 Rabs (bpow (Fexp {| Fnum := m; Fexp := e |})))%R
rewrite <- abs_IZR.beta:radix
m, e:Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) *
 bpow (Fexp {| Fnum := Z.abs m; Fexp := e |}))%R =
(IZR (Z.abs (Fnum {| Fnum := m; Fexp := e |})) *
 Rabs (bpow (Fexp {| Fnum := m; Fexp := e |})))%R
simpl.beta:radix
m, e:Z
(IZR (Z.abs m) * bpow e)%R =
(IZR (Z.abs m) * Rabs (bpow e))%R
apply f_equal.beta:radix
m, e:Z
bpow e = Rabs (bpow e)
apply sym_eq; apply Rabs_right.beta:radix
m, e:Z
(bpow e >= 0)%R
apply Rle_ge.beta:radix
m, e:Z
(0 <= bpow e)%R
apply bpow_ge_0.
Qed.

Theorem F2R_Zopp :
  forall m e : Z,
  F2R (Float beta (Z.opp m) e) = Ropp (F2R (Float beta m e)).beta:radix
forall m e : Z,
F2R {| Fnum := - m; Fexp := e |} =
(- F2R {| Fnum := m; Fexp := e |})%R
Proof.beta:radix
forall m e : Z,
F2R {| Fnum := - m; Fexp := e |} =
(- F2R {| Fnum := m; Fexp := e |})%R
intros m e.beta:radix
m, e:Z
F2R {| Fnum := - m; Fexp := e |} =
(- F2R {| Fnum := m; Fexp := e |})%R
unfold F2R.beta:radix
m, e:Z
(IZR (Fnum {| Fnum := - m; Fexp := e |}) *
 bpow (Fexp {| Fnum := - m; Fexp := e |}))%R =
(-
 (IZR (Fnum {| Fnum := m; Fexp := e |}) *
  bpow (Fexp {| Fnum := m; Fexp := e |})))%R simpl.beta:radix
m, e:Z
(IZR (- m) * bpow e)%R = (- (IZR m * bpow e))%R
rewrite <- Ropp_mult_distr_l_reverse.beta:radix
m, e:Z
(IZR (- m) * bpow e)%R = (- IZR m * bpow e)%R
now rewrite opp_IZR.
Qed.

Theorem F2R_cond_Zopp :
  forall b m e,
  F2R (Float beta (cond_Zopp b m) e) = cond_Ropp b (F2R (Float beta m e)).beta:radix
forall (b : bool) (m e : Z),
F2R
  {| Fnum := SpecFloatCopy.cond_Zopp b m; Fexp := e |} =
cond_Ropp b (F2R {| Fnum := m; Fexp := e |})
Proof.beta:radix
forall (b : bool) (m e : Z),
F2R
  {| Fnum := SpecFloatCopy.cond_Zopp b m; Fexp := e |} =
cond_Ropp b (F2R {| Fnum := m; Fexp := e |})
intros [|] m e ; unfold F2R ; simpl.beta:radix
m, e:Z
(IZR (- m) * bpow e)%R = (- (IZR m * bpow e))%R
beta:radix
m, e:Z
(IZR m * bpow e)%R = (IZR m * bpow e)%R
now rewrite opp_IZR, Ropp_mult_distr_l_reverse.beta:radix
m, e:Z
(IZR m * bpow e)%R = (IZR m * bpow e)%R
apply refl_equal.
Qed.

Sign facts

Theorem F2R_0 :
  forall e : Z,
  F2R (Float beta 0 e) = 0%R.beta:radix
forall e : Z, F2R {| Fnum := 0; Fexp := e |} = 0%R
Proof.beta:radix
forall e : Z, F2R {| Fnum := 0; Fexp := e |} = 0%R
intros e.beta:radix
e:Z
F2R {| Fnum := 0; Fexp := e |} = 0%R
unfold F2R.beta:radix
e:Z
(IZR (Fnum {| Fnum := 0; Fexp := e |}) *
 bpow (Fexp {| Fnum := 0; Fexp := e |}))%R = 0%R simpl.beta:radix
e:Z
(0 * bpow e)%R = 0%R
apply Rmult_0_l.
Qed.

Theorem eq_0_F2R :
  forall m e : Z,
  F2R (Float beta m e) = 0%R ->
  m = Z0.beta:radix
forall m e : Z,
F2R {| Fnum := m; Fexp := e |} = 0%R -> m = 0%Z
Proof.beta:radix
forall m e : Z,
F2R {| Fnum := m; Fexp := e |} = 0%R -> m = 0%Z
intros m e H.beta:radix
m, e:Z
H:F2R {| Fnum := m; Fexp := e |} = 0%R
m = 0%Z
apply eq_F2R with e.beta:radix
m, e:Z
H:F2R {| Fnum := m; Fexp := e |} = 0%R
F2R {| Fnum := m; Fexp := e |} =
F2R {| Fnum := 0; Fexp := e |}
now rewrite F2R_0.
Qed.

Theorem ge_0_F2R :
  forall m e : Z,
  (0 <= F2R (Float beta m e))%R ->
  (0 <= m)%Z.beta:radix
forall m e : Z,
(0 <= F2R {| Fnum := m; Fexp := e |})%R -> (0 <= m)%Z
Proof.beta:radix
forall m e : Z,
(0 <= F2R {| Fnum := m; Fexp := e |})%R -> (0 <= m)%Z
intros m e H.beta:radix
m, e:Z
H:(0 <= F2R {| Fnum := m; Fexp := e |})%R
(0 <= m)%Z
apply le_F2R with e.beta:radix
m, e:Z
H:(0 <= F2R {| Fnum := m; Fexp := e |})%R
(F2R {| Fnum := 0; Fexp := e |} <=
 F2R {| Fnum := m; Fexp := e |})%R
now rewrite F2R_0.
Qed.

Theorem le_0_F2R :
  forall m e : Z,
  (F2R (Float beta m e) <= 0)%R ->
  (m <= 0)%Z.beta:radix
forall m e : Z,
(F2R {| Fnum := m; Fexp := e |} <= 0)%R -> (m <= 0)%Z
Proof.beta:radix
forall m e : Z,
(F2R {| Fnum := m; Fexp := e |} <= 0)%R -> (m <= 0)%Z
intros m e H.beta:radix
m, e:Z
H:(F2R {| Fnum := m; Fexp := e |} <= 0)%R
(m <= 0)%Z
apply le_F2R with e.beta:radix
m, e:Z
H:(F2R {| Fnum := m; Fexp := e |} <= 0)%R
(F2R {| Fnum := m; Fexp := e |} <=
 F2R {| Fnum := 0; Fexp := e |})%R
now rewrite F2R_0.
Qed.

Theorem gt_0_F2R :
  forall m e : Z,
  (0 < F2R (Float beta m e))%R ->
  (0 < m)%Z.beta:radix
forall m e : Z,
(0 < F2R {| Fnum := m; Fexp := e |})%R -> (0 < m)%Z
Proof.beta:radix
forall m e : Z,
(0 < F2R {| Fnum := m; Fexp := e |})%R -> (0 < m)%Z
intros m e H.beta:radix
m, e:Z
H:(0 < F2R {| Fnum := m; Fexp := e |})%R
(0 < m)%Z
apply lt_F2R with e.beta:radix
m, e:Z
H:(0 < F2R {| Fnum := m; Fexp := e |})%R
(F2R {| Fnum := 0; Fexp := e |} <
 F2R {| Fnum := m; Fexp := e |})%R
now rewrite F2R_0.
Qed.

Theorem lt_0_F2R :
  forall m e : Z,
  (F2R (Float beta m e) < 0)%R ->
  (m < 0)%Z.beta:radix
forall m e : Z,
(F2R {| Fnum := m; Fexp := e |} < 0)%R -> (m < 0)%Z
Proof.beta:radix
forall m e : Z,
(F2R {| Fnum := m; Fexp := e |} < 0)%R -> (m < 0)%Z
intros m e H.beta:radix
m, e:Z
H:(F2R {| Fnum := m; Fexp := e |} < 0)%R
(m < 0)%Z
apply lt_F2R with e.beta:radix
m, e:Z
H:(F2R {| Fnum := m; Fexp := e |} < 0)%R
(F2R {| Fnum := m; Fexp := e |} <
 F2R {| Fnum := 0; Fexp := e |})%R
now rewrite F2R_0.
Qed.

Theorem F2R_ge_0 :
  forall f : float beta,
  (0 <= Fnum f)%Z ->
  (0 <= F2R f)%R.beta:radix
forall f : float beta,
(0 <= Fnum f)%Z -> (0 <= F2R f)%R
Proof.beta:radix
forall f : float beta,
(0 <= Fnum f)%Z -> (0 <= F2R f)%R
intros f H.beta:radix
f:float beta
H:(0 <= Fnum f)%Z
(0 <= F2R f)%R
rewrite <- F2R_0 with (Fexp f).beta:radix
f:float beta
H:(0 <= Fnum f)%Z
(F2R {| Fnum := 0; Fexp := Fexp f |} <= F2R f)%R
now apply F2R_le.
Qed.

Theorem F2R_le_0 :
  forall f : float beta,
  (Fnum f <= 0)%Z ->
  (F2R f <= 0)%R.beta:radix
forall f : float beta,
(Fnum f <= 0)%Z -> (F2R f <= 0)%R
Proof.beta:radix
forall f : float beta,
(Fnum f <= 0)%Z -> (F2R f <= 0)%R
intros f H.beta:radix
f:float beta
H:(Fnum f <= 0)%Z
(F2R f <= 0)%R
rewrite <- F2R_0 with (Fexp f).beta:radix
f:float beta
H:(Fnum f <= 0)%Z
(F2R f <= F2R {| Fnum := 0; Fexp := Fexp f |})%R
now apply F2R_le.
Qed.

Theorem F2R_gt_0 :
  forall f : float beta,
  (0 < Fnum f)%Z ->
  (0 < F2R f)%R.beta:radix
forall f : float beta, (0 < Fnum f)%Z -> (0 < F2R f)%R
Proof.beta:radix
forall f : float beta, (0 < Fnum f)%Z -> (0 < F2R f)%R
intros f H.beta:radix
f:float beta
H:(0 < Fnum f)%Z
(0 < F2R f)%R
rewrite <- F2R_0 with (Fexp f).beta:radix
f:float beta
H:(0 < Fnum f)%Z
(F2R {| Fnum := 0; Fexp := Fexp f |} < F2R f)%R
now apply F2R_lt.
Qed.

Theorem F2R_lt_0 :
  forall f : float beta,
  (Fnum f < 0)%Z ->
  (F2R f < 0)%R.beta:radix
forall f : float beta, (Fnum f < 0)%Z -> (F2R f < 0)%R
Proof.beta:radix
forall f : float beta, (Fnum f < 0)%Z -> (F2R f < 0)%R
intros f H.beta:radix
f:float beta
H:(Fnum f < 0)%Z
(F2R f < 0)%R
rewrite <- F2R_0 with (Fexp f).beta:radix
f:float beta
H:(Fnum f < 0)%Z
(F2R f < F2R {| Fnum := 0; Fexp := Fexp f |})%R
now apply F2R_lt.
Qed.

Theorem F2R_neq_0 :
 forall f : float beta,
  (Fnum f <> 0)%Z ->
  (F2R f <> 0)%R.beta:radix
forall f : float beta, Fnum f <> 0%Z -> F2R f <> 0%R
Proof.beta:radix
forall f : float beta, Fnum f <> 0%Z -> F2R f <> 0%R
intros f H H1.beta:radix
f:float beta
H:Fnum f <> 0%Z
H1:F2R f = 0%R
False
apply H.beta:radix
f:float beta
H:Fnum f <> 0%Z
H1:F2R f = 0%R
Fnum f = 0%Z
now apply eq_0_F2R with (Fexp f).
Qed.


Lemma Fnum_ge_0: forall (f : float beta),
  (0 <= F2R f)%R -> (0 <= Fnum f)%Z.beta:radix
forall f : float beta,
(0 <= F2R f)%R -> (0 <= Fnum f)%Z
Proof.beta:radix
forall f : float beta,
(0 <= F2R f)%R -> (0 <= Fnum f)%Z
intros f H.beta:radix
f:float beta
H:(0 <= F2R f)%R
(0 <= Fnum f)%Z
case (Zle_or_lt 0 (Fnum f)); trivial.beta:radix
f:float beta
H:(0 <= F2R f)%R
(Fnum f < 0)%Z -> (0 <= Fnum f)%Z
intros H1; contradict H.beta:radix
f:float beta
H1:(Fnum f < 0)%Z
~ (0 <= F2R f)%R
apply Rlt_not_le.beta:radix
f:float beta
H1:(Fnum f < 0)%Z
(F2R f < 0)%R
now apply F2R_lt_0.
Qed.

Lemma Fnum_le_0: forall (f : float beta),
  (F2R f <= 0)%R -> (Fnum f <= 0)%Z.beta:radix
forall f : float beta,
(F2R f <= 0)%R -> (Fnum f <= 0)%Z
Proof.beta:radix
forall f : float beta,
(F2R f <= 0)%R -> (Fnum f <= 0)%Z
intros f H.beta:radix
f:float beta
H:(F2R f <= 0)%R
(Fnum f <= 0)%Z
case (Zle_or_lt (Fnum f) 0); trivial.beta:radix
f:float beta
H:(F2R f <= 0)%R
(0 < Fnum f)%Z -> (Fnum f <= 0)%Z
intros H1; contradict H.beta:radix
f:float beta
H1:(0 < Fnum f)%Z
~ (F2R f <= 0)%R
apply Rlt_not_le.beta:radix
f:float beta
H1:(0 < Fnum f)%Z
(0 < F2R f)%R
now apply F2R_gt_0.
Qed.

Floats and bpow

Theorem F2R_bpow :
  forall e : Z,
  F2R (Float beta 1 e) = bpow e.beta:radix
forall e : Z, F2R {| Fnum := 1; Fexp := e |} = bpow e
Proof.beta:radix
forall e : Z, F2R {| Fnum := 1; Fexp := e |} = bpow e
intros e.beta:radix
e:Z
F2R {| Fnum := 1; Fexp := e |} = bpow e
unfold F2R.beta:radix
e:Z
(IZR (Fnum {| Fnum := 1; Fexp := e |}) *
 bpow (Fexp {| Fnum := 1; Fexp := e |}))%R = bpow e simpl.beta:radix
e:Z
(1 * bpow e)%R = bpow e
apply Rmult_1_l.
Qed.

Theorem bpow_le_F2R :
  forall m e : Z,
  (0 < m)%Z ->
  (bpow e <= F2R (Float beta m e))%R.beta:radix
forall m e : Z,
(0 < m)%Z ->
(bpow e <= F2R {| Fnum := m; Fexp := e |})%R
Proof.beta:radix
forall m e : Z,
(0 < m)%Z ->
(bpow e <= F2R {| Fnum := m; Fexp := e |})%R
intros m e H.beta:radix
m, e:Z
H:(0 < m)%Z
(bpow e <= F2R {| Fnum := m; Fexp := e |})%R
rewrite <- F2R_bpow.beta:radix
m, e:Z
H:(0 < m)%Z
(F2R {| Fnum := 1; Fexp := e |} <=
 F2R {| Fnum := m; Fexp := e |})%R
apply F2R_le.beta:radix
m, e:Z
H:(0 < m)%Z
(1 <= m)%Z
now apply (Zlt_le_succ 0).
Qed.

Theorem F2R_p1_le_bpow :
  forall m e1 e2 : Z,
  (0 < m)%Z ->
  (F2R (Float beta m e1) < bpow e2)%R ->
  (F2R (Float beta (m + 1) e1) <= bpow e2)%R.beta:radix
forall m e1 e2 : Z,
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
Proof.beta:radix
forall m e1 e2 : Z,
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
intros m e1 e2 Hm.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
intros H.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
assert (He : (e1 <= e2)%Z).beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(e1 <= e2)%Z
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
(* . *)
apply (le_bpow beta).beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(bpow e1 <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
apply Rle_trans with (F2R (Float beta m e1)).beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(bpow e1 <= F2R {| Fnum := m; Fexp := e1 |})%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
unfold F2R.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(bpow e1 <=
 IZR (Fnum {| Fnum := m; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m; Fexp := e1 |}))%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R simpl.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(bpow e1 <= IZR m * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
rewrite <- (Rmult_1_l (bpow e1)) at 1.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(1 * bpow e1 <= IZR m * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
apply Rmult_le_compat_r.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(0 <= bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(1 <= IZR m)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
apply bpow_ge_0.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(1 <= IZR m)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
apply IZR_le.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(1 <= m)%Z
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
now apply (Zlt_le_succ 0).beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
(F2R {| Fnum := m; Fexp := e1 |} <= bpow e2)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
now apply Rlt_le.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
H:(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R
He:(e1 <= e2)%Z
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
(* . *)
revert H.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(F2R {| Fnum := m; Fexp := e1 |} < bpow e2)%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <= bpow e2)%R
replace e2 with (e2 - e1 + e1)%Z by ring.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(F2R {| Fnum := m; Fexp := e1 |} < bpow (e2 - e1 + e1))%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <=
 bpow (e2 - e1 + e1))%R
rewrite bpow_plus.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(F2R {| Fnum := m; Fexp := e1 |} <
 bpow (e2 - e1) * bpow e1)%R ->
(F2R {| Fnum := m + 1; Fexp := e1 |} <=
 bpow (e2 - e1) * bpow e1)%R
unfold F2R.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(IZR (Fnum {| Fnum := m; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m; Fexp := e1 |}) <
 bpow (e2 - e1) * bpow e1)%R ->
(IZR (Fnum {| Fnum := m + 1; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m + 1; Fexp := e1 |}) <=
 bpow (e2 - e1) * bpow e1)%R simpl.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(IZR m * bpow e1 < bpow (e2 - e1) * bpow e1)%R ->
(IZR (m + 1) * bpow e1 <= bpow (e2 - e1) * bpow e1)%R
rewrite <- (IZR_Zpower beta (e2 - e1)).beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(IZR m * bpow e1 < IZR (beta ^ (e2 - e1)) * bpow e1)%R ->
(IZR (m + 1) * bpow e1 <=
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
intros H.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(IZR (m + 1) * bpow e1 <=
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply Rmult_le_compat_r.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(0 <= bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(IZR (m + 1) <= IZR (beta ^ (e2 - e1)))%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply bpow_ge_0.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(IZR (m + 1) <= IZR (beta ^ (e2 - e1)))%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply Rmult_lt_reg_r in H.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m < IZR (beta ^ (e2 - e1)))%R
(IZR (m + 1) <= IZR (beta ^ (e2 - e1)))%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply IZR_le.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m < IZR (beta ^ (e2 - e1)))%R
(m + 1 <= beta ^ (e2 - e1))%Z
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply Zlt_le_succ.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m < IZR (beta ^ (e2 - e1)))%R
(m < beta ^ (e2 - e1))%Z
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
now apply lt_IZR.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
H:(IZR m * bpow e1 <
 IZR (beta ^ (e2 - e1)) * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
apply bpow_gt_0.beta:radix
m, e1, e2:Z
Hm:(0 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
now apply Zle_minus_le_0.
Qed.

Theorem bpow_le_F2R_m1 :
  forall m e1 e2 : Z,
  (1 < m)%Z ->
  (bpow e2 < F2R (Float beta m e1))%R ->
  (bpow e2 <= F2R (Float beta (m - 1) e1))%R.beta:radix
forall m e1 e2 : Z,
(1 < m)%Z ->
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
Proof.beta:radix
forall m e1 e2 : Z,
(1 < m)%Z ->
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
intros m e1 e2 Hm.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
case (Zle_or_lt e1 e2); intros He.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
replace e2 with (e2 - e1 + e1)%Z by ring.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(bpow (e2 - e1 + e1) < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow (e2 - e1 + e1) <=
 F2R {| Fnum := m - 1; Fexp := e1 |})%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
rewrite bpow_plus.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(bpow (e2 - e1) * bpow e1 <
 F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow (e2 - e1) * bpow e1 <=
 F2R {| Fnum := m - 1; Fexp := e1 |})%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
unfold F2R.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(bpow (e2 - e1) * bpow e1 <
 IZR (Fnum {| Fnum := m; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m; Fexp := e1 |}))%R ->
(bpow (e2 - e1) * bpow e1 <=
 IZR (Fnum {| Fnum := m - 1; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m - 1; Fexp := e1 |}))%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R simpl.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(bpow (e2 - e1) * bpow e1 < IZR m * bpow e1)%R ->
(bpow (e2 - e1) * bpow e1 <= IZR (m - 1) * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
rewrite <- (IZR_Zpower beta (e2 - e1)).beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(IZR (beta ^ (e2 - e1)) * bpow e1 < IZR m * bpow e1)%R ->
(IZR (beta ^ (e2 - e1)) * bpow e1 <=
 IZR (m - 1) * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
intros H.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(IZR (beta ^ (e2 - e1)) * bpow e1 <=
 IZR (m - 1) * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply Rmult_le_compat_r.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 <= bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(IZR (beta ^ (e2 - e1)) <= IZR (m - 1))%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply bpow_ge_0.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(IZR (beta ^ (e2 - e1)) <= IZR (m - 1))%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply Rmult_lt_reg_r in H.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) < IZR m)%R
(IZR (beta ^ (e2 - e1)) <= IZR (m - 1))%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply IZR_le.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) < IZR m)%R
(beta ^ (e2 - e1) <= m - 1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
rewrite (Zpred_succ (Zpower _ _)).beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) < IZR m)%R
(Z.pred (Z.succ (beta ^ (e2 - e1))) <= m - 1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply Zplus_le_compat_r.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) < IZR m)%R
(Z.succ (beta ^ (e2 - e1)) <= m)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply Zlt_le_succ.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) < IZR m)%R
(beta ^ (e2 - e1) < m)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
now apply lt_IZR.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
H:(IZR (beta ^ (e2 - e1)) * bpow e1 <
 IZR m * bpow e1)%R
(0 < bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply bpow_gt_0.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e1 <= e2)%Z
(0 <= e2 - e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
now apply Zle_minus_le_0.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R ->
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
intros H.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(bpow e2 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply Rle_trans with (1*bpow e1)%R.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(bpow e2 <= 1 * bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
rewrite Rmult_1_l.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(bpow e2 <= bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
apply bpow_le.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(e2 <= e1)%Z
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
now apply Zlt_le_weak.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <= F2R {| Fnum := m - 1; Fexp := e1 |})%R
unfold F2R.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <=
 IZR (Fnum {| Fnum := m - 1; Fexp := e1 |}) *
 bpow (Fexp {| Fnum := m - 1; Fexp := e1 |}))%R simpl.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 * bpow e1 <= IZR (m - 1) * bpow e1)%R
apply Rmult_le_compat_r.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(0 <= bpow e1)%R
beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 <= IZR (m - 1))%R
apply bpow_ge_0.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 <= IZR (m - 1))%R
apply IZR_le.beta:radix
m, e1, e2:Z
Hm:(1 < m)%Z
He:(e2 < e1)%Z
H:(bpow e2 < F2R {| Fnum := m; Fexp := e1 |})%R
(1 <= m - 1)%Z
omega.
Qed.

Theorem F2R_lt_bpow :
  forall f : float beta, forall e',
  (Z.abs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
  (Rabs (F2R f) < bpow e')%R.beta:radix
forall (f : float beta) (e' : Z),
(Z.abs (Fnum f) < beta ^ (e' - Fexp f))%Z ->
(Rabs (F2R f) < bpow e')%R
Proof.beta:radix
forall (f : float beta) (e' : Z),
(Z.abs (Fnum f) < beta ^ (e' - Fexp f))%Z ->
(Rabs (F2R f) < bpow e')%R
intros (m, e) e' Hm.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
(Rabs (F2R {| Fnum := m; Fexp := e |}) < bpow e')%R
rewrite <- F2R_Zabs.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
destruct (Zle_or_lt e e') as [He|He].beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
unfold F2R.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) *
 bpow (Fexp {| Fnum := Z.abs m; Fexp := e |}) <
 bpow e')%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R simpl.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) * bpow e < bpow e')%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
apply Rmult_lt_reg_r with (bpow (-e)).beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(0 < bpow (- e))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) * bpow e * bpow (- e) <
 bpow e' * bpow (- e))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
apply bpow_gt_0.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) * bpow e * bpow (- e) <
 bpow e' * bpow (- e))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) < bpow (e' + - e))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
rewrite <-IZR_Zpower.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) < IZR (beta ^ (e' + - e)))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(0 <= e' + - e)%Z
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R 2: now apply Zle_left.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e <= e')%Z
(IZR (Z.abs m) < IZR (beta ^ (e' + - e)))%R
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
now apply IZR_lt.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} < bpow e')%R
elim Zlt_not_le with (1 := Hm).beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}) <=
 Z.abs (Fnum {| Fnum := m; Fexp := e |}))%Z
simpl.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(beta ^ (e' - e) <= Z.abs m)%Z
cut (e' - e < 0)%Z.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(e' - e < 0)%Z -> (beta ^ (e' - e) <= Z.abs m)%Z
beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(e' - e < 0)%Z 2: omega.beta:radix
m, e, e':Z
Hm:(Z.abs (Fnum {| Fnum := m; Fexp := e |}) <
 beta ^ (e' - Fexp {| Fnum := m; Fexp := e |}))%Z
He:(e' < e)%Z
(e' - e < 0)%Z -> (beta ^ (e' - e) <= Z.abs m)%Z
clear.beta:radix
m, e, e':Z
(e' - e < 0)%Z -> (beta ^ (e' - e) <= Z.abs m)%Z
case (e' - e)%Z ; try easy.beta:radix
m, e, e':Z
forall p : positive,
(Z.neg p < 0)%Z -> (beta ^ Z.neg p <= Z.abs m)%Z
intros p _.beta:radix
m, e, e':Z
p:positive
(beta ^ Z.neg p <= Z.abs m)%Z
apply Zabs_pos.
Qed.

Theorem F2R_change_exp :
  forall e' m e : Z,
  (e' <= e)%Z ->
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').beta:radix
forall e' m e : Z,
(e' <= e)%Z ->
F2R {| Fnum := m; Fexp := e |} =
F2R {| Fnum := m * beta ^ (e - e'); Fexp := e' |}
Proof.beta:radix
forall e' m e : Z,
(e' <= e)%Z ->
F2R {| Fnum := m; Fexp := e |} =
F2R {| Fnum := m * beta ^ (e - e'); Fexp := e' |}
intros e' m e He.beta:radix
e', m, e:Z
He:(e' <= e)%Z
F2R {| Fnum := m; Fexp := e |} =
F2R {| Fnum := m * beta ^ (e - e'); Fexp := e' |}
unfold F2R.beta:radix
e', m, e:Z
He:(e' <= e)%Z
(IZR (Fnum {| Fnum := m; Fexp := e |}) *
 bpow (Fexp {| Fnum := m; Fexp := e |}))%R =
(IZR
   (Fnum {| Fnum := m * beta ^ (e - e'); Fexp := e' |}) *
 bpow
   (Fexp {| Fnum := m * beta ^ (e - e'); Fexp := e' |}))%R simpl.beta:radix
e', m, e:Z
He:(e' <= e)%Z
(IZR m * bpow e)%R =
(IZR (m * beta ^ (e - e')) * bpow e')%R
rewrite mult_IZR, IZR_Zpower, Rmult_assoc.beta:radix
e', m, e:Z
He:(e' <= e)%Z
(IZR m * bpow e)%R =
(IZR m * (bpow (e - e') * bpow e'))%R
beta:radix
e', m, e:Z
He:(e' <= e)%Z
(0 <= e - e')%Z
apply f_equal.beta:radix
e', m, e:Z
He:(e' <= e)%Z
bpow e = (bpow (e - e') * bpow e')%R
beta:radix
e', m, e:Z
He:(e' <= e)%Z
(0 <= e - e')%Z
pattern e at 1 ; replace e with (e - e' + e')%Z by ring.beta:radix
e', m, e:Z
He:(e' <= e)%Z
bpow (e - e' + e') = (bpow (e - e') * bpow e')%R
beta:radix
e', m, e:Z
He:(e' <= e)%Z
(0 <= e - e')%Z
apply bpow_plus.beta:radix
e', m, e:Z
He:(e' <= e)%Z
(0 <= e - e')%Z
now apply Zle_minus_le_0.
Qed.

Theorem F2R_prec_normalize :
  forall m e e' p : Z,
  (Z.abs m < Zpower beta p)%Z ->
  (bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).beta:radix
forall m e e' p : Z,
(Z.abs m < beta ^ p)%Z ->
(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R ->
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
Proof.beta:radix
forall m e e' p : Z,
(Z.abs m < beta ^ p)%Z ->
(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R ->
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
intros m e e' p Hm Hf.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
assert (Hp: (0 <= p)%Z).beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
(0 <= p)%Z
beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
destruct p ; try easy.beta:radix
m, e, e':Z
p:positive
Hm:(Z.abs m < beta ^ Z.neg p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
(0 <= Z.neg p)%Z
beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
now elim (Zle_not_lt _ _ (Zabs_pos m)).beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - e' + p);
  Fexp := e' - p |}
(* . *)
replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
F2R {| Fnum := m; Fexp := e |} =
F2R
  {|
  Fnum := m * beta ^ (e - (e' - p));
  Fexp := e' - p |}
apply F2R_change_exp.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(e' - p <= e)%Z
cut (e' - 1 < e + p)%Z.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(e' - 1 < e + p)%Z -> (e' - p <= e)%Z
beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(e' - 1 < e + p)%Z omega.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(e' - 1 < e + p)%Z
apply (lt_bpow beta).beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(bpow (e' - 1) < bpow (e + p))%R
apply Rle_lt_trans with (1 := Hf).beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(Rabs (F2R {| Fnum := m; Fexp := e |}) < bpow (e + p))%R
rewrite <- F2R_Zabs, Zplus_comm, bpow_plus.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(F2R {| Fnum := Z.abs m; Fexp := e |} <
 bpow p * bpow e)%R
apply Rmult_lt_compat_r.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(0 < bpow e)%R
beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) < bpow p)%R
apply bpow_gt_0.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) < bpow p)%R
rewrite <- IZR_Zpower.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(IZR (Fnum {| Fnum := Z.abs m; Fexp := e |}) <
 IZR (beta ^ p))%R
beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(0 <= p)%Z
now apply IZR_lt.beta:radix
m, e, e', p:Z
Hm:(Z.abs m < beta ^ p)%Z
Hf:(bpow (e' - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}))%R
Hp:(0 <= p)%Z
(0 <= p)%Z
exact Hp.
Qed.

Floats and mag

Theorem mag_F2R_bounds :
  forall x m e, (0 < m)%Z ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
  mag beta x = mag beta (F2R (Float beta m e)) :> Z.beta:radix
forall (x : R) (m e : Z),
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e |} <= x <
 F2R {| Fnum := m + 1; Fexp := e |})%R ->
mag beta x = mag beta (F2R {| Fnum := m; Fexp := e |})
Proof.beta:radix
forall (x : R) (m e : Z),
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e |} <= x <
 F2R {| Fnum := m + 1; Fexp := e |})%R ->
mag beta x = mag beta (F2R {| Fnum := m; Fexp := e |})
intros x m e Hp (Hx,Hx2).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
mag beta x = mag beta (F2R {| Fnum := m; Fexp := e |})
destruct (mag beta (F2R (Float beta m e))) as (ex, He).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
mag beta x =
Build_mag_prop beta (F2R {| Fnum := m; Fexp := e |})
  ex He
simpl.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
mag beta x = ex
apply mag_unique.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
assert (Hp1: (0 < F2R (Float beta m e))%R).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
(0 < F2R {| Fnum := m; Fexp := e |})%R
beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
now apply F2R_gt_0.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:F2R {| Fnum := m; Fexp := e |} <> 0%R ->
(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
specialize (He (Rgt_not_eq _ _ Hp1)).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
rewrite Rabs_pos_eq in He.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:(bpow (ex - 1) <=
 F2R {| Fnum := m; Fexp := e |} < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:(bpow (ex - 1) <=
 Rabs (F2R {| Fnum := m; Fexp := e |}) < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(0 <= F2R {| Fnum := m; Fexp := e |})%R 2: now apply Rlt_le.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He:(bpow (ex - 1) <=
 F2R {| Fnum := m; Fexp := e |} < 
 bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
destruct He as (He1, He2).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
assert (Hx1: (0 < x)%R).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
(0 < x)%R
beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
now apply Rlt_le_trans with (2 := Hx).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(bpow (ex - 1) <= Rabs x < bpow ex)%R
rewrite Rabs_pos_eq.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(bpow (ex - 1) <= x < bpow ex)%R
beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(0 <= x)%R 2: now apply Rlt_le.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(bpow (ex - 1) <= x < bpow ex)%R
split.beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(bpow (ex - 1) <= x)%R
beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(x < bpow ex)%R
now apply Rle_trans with (1 := He1).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(x < bpow ex)%R
apply Rlt_le_trans with (1 := Hx2).beta:radix
x:R
m, e:Z
Hp:(0 < m)%Z
Hx:(F2R {| Fnum := m; Fexp := e |} <= x)%R
Hx2:(x < F2R {| Fnum := m + 1; Fexp := e |})%R
ex:Z
He1:(bpow (ex - 1) <= F2R {| Fnum := m; Fexp := e |})%R
He2:(F2R {| Fnum := m; Fexp := e |} < bpow ex)%R
Hp1:(0 < F2R {| Fnum := m; Fexp := e |})%R
Hx1:(0 < x)%R
(F2R {| Fnum := m + 1; Fexp := e |} <= bpow ex)%R
now apply F2R_p1_le_bpow.
Qed.

Theorem mag_F2R :
  forall m e : Z,
  m <> Z0 ->
  (mag beta (F2R (Float beta m e)) = mag beta (IZR m) + e :> Z)%Z.beta:radix
forall m e : Z,
m <> 0%Z ->
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(mag beta (IZR m) + e)%Z
Proof.beta:radix
forall m e : Z,
m <> 0%Z ->
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(mag beta (IZR m) + e)%Z
intros m e H.beta:radix
m, e:Z
H:m <> 0%Z
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(mag beta (IZR m) + e)%Z
unfold F2R ; simpl.beta:radix
m, e:Z
H:m <> 0%Z
mag beta (IZR m * bpow e) = (mag beta (IZR m) + e)%Z
apply mag_mult_bpow.beta:radix
m, e:Z
H:m <> 0%Z
IZR m <> 0%R
now apply IZR_neq.
Qed.

Theorem Zdigits_mag :
  forall n,
  n <> Z0 ->
  Zdigits beta n = mag beta (IZR n).beta:radix
forall n : Z,
n <> 0%Z -> Zdigits beta n = mag beta (IZR n)
Proof.beta:radix
forall n : Z,
n <> 0%Z -> Zdigits beta n = mag beta (IZR n)
intros n Hn.beta:radix
n:Z
Hn:n <> 0%Z
Zdigits beta n = mag beta (IZR n)
destruct (mag beta (IZR n)) as (e, He) ; simpl.beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:IZR n <> 0%R ->
(bpow (e - 1) <= Rabs (IZR n) < bpow e)%R
Zdigits beta n = e
specialize (He (IZR_neq _ _ Hn)).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= Rabs (IZR n) < bpow e)%R
Zdigits beta n = e
rewrite <- abs_IZR in He.beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Zdigits beta n = e
assert (Hd := Zdigits_correct beta n).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Zdigits beta n = e
assert (Hd' := Zdigits_gt_0 beta n).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
Zdigits beta n = e
apply Zle_antisym ; apply (bpow_lt_bpow beta).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (Zdigits beta n - 1) < bpow e)%R
beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (e - 1) < bpow (Zdigits beta n))%R
apply Rle_lt_trans with (2 := proj2 He).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (Zdigits beta n - 1) <= IZR (Z.abs n))%R
beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (e - 1) < bpow (Zdigits beta n))%R
rewrite <- IZR_Zpower by omega.beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(IZR (beta ^ (Zdigits beta n - 1)) <= IZR (Z.abs n))%R
beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (e - 1) < bpow (Zdigits beta n))%R
now apply IZR_le.beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(bpow (e - 1) < bpow (Zdigits beta n))%R
apply Rle_lt_trans with (1 := proj1 He).beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(IZR (Z.abs n) < bpow (Zdigits beta n))%R
rewrite <- IZR_Zpower by omega.beta:radix
n:Z
Hn:n <> 0%Z
e:Z
He:(bpow (e - 1) <= IZR (Z.abs n) < bpow e)%R
Hd:(beta ^ (Zdigits beta n - 1) <= 
 Z.abs n < beta ^ Zdigits beta n)%Z
Hd':n <> 0%Z -> (0 < Zdigits beta n)%Z
(IZR (Z.abs n) < IZR (beta ^ Zdigits beta n))%R
now apply IZR_lt.
Qed.

Theorem mag_F2R_Zdigits :
  forall m e, m <> Z0 ->
  (mag beta (F2R (Float beta m e)) = Zdigits beta m + e :> Z)%Z.beta:radix
forall m e : Z,
m <> 0%Z ->
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(Zdigits beta m + e)%Z
Proof.beta:radix
forall m e : Z,
m <> 0%Z ->
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(Zdigits beta m + e)%Z
intros m e Hm.beta:radix
m, e:Z
Hm:m <> 0%Z
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(Zdigits beta m + e)%Z
rewrite mag_F2R with (1 := Hm).beta:radix
m, e:Z
Hm:m <> 0%Z
(mag beta (IZR m) + e)%Z = (Zdigits beta m + e)%Z
apply (f_equal (fun v => Zplus v e)).beta:radix
m, e:Z
Hm:m <> 0%Z
mag beta (IZR m) = Zdigits beta m
apply sym_eq.beta:radix
m, e:Z
Hm:m <> 0%Z
Zdigits beta m = mag beta (IZR m)
now apply Zdigits_mag.
Qed.

Theorem mag_F2R_bounds_Zdigits :
  forall x m e, (0 < m)%Z ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
  mag beta x = (Zdigits beta m + e)%Z :> Z.beta:radix
forall (x : R) (m e : Z),
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e |} <= x <
 F2R {| Fnum := m + 1; Fexp := e |})%R ->
mag beta x = (Zdigits beta m + e)%Z
Proof.beta:radix
forall (x : R) (m e : Z),
(0 < m)%Z ->
(F2R {| Fnum := m; Fexp := e |} <= x <
 F2R {| Fnum := m + 1; Fexp := e |})%R ->
mag beta x = (Zdigits beta m + e)%Z
intros x m e Hm Bx.beta:radix
x:R
m, e:Z
Hm:(0 < m)%Z
Bx:(F2R {| Fnum := m; Fexp := e |} <= x <
 F2R {| Fnum := m + 1; Fexp := e |})%R
mag beta x = (Zdigits beta m + e)%Z
apply mag_F2R_bounds with (1 := Hm) in Bx.beta:radix
x:R
m, e:Z
Hm:(0 < m)%Z
Bx:mag beta x =
mag beta (F2R {| Fnum := m; Fexp := e |})
mag beta x = (Zdigits beta m + e)%Z
rewrite Bx.beta:radix
x:R
m, e:Z
Hm:(0 < m)%Z
Bx:mag beta x =
mag beta (F2R {| Fnum := m; Fexp := e |})
mag beta (F2R {| Fnum := m; Fexp := e |}) =
(Zdigits beta m + e)%Z
apply mag_F2R_Zdigits.beta:radix
x:R
m, e:Z
Hm:(0 < m)%Z
Bx:mag beta x =
mag beta (F2R {| Fnum := m; Fexp := e |})
m <> 0%Z
now apply Zgt_not_eq.
Qed.

Theorem float_distribution_pos :
  forall m1 e1 m2 e2 : Z,
  (0 < m1)%Z ->
  (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R ->
  (e2 < e1)%Z /\ (e1 + mag beta (IZR m1) = e2 + mag beta (IZR m2))%Z.beta:radix
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R ->
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
Proof.beta:radix
forall m1 e1 m2 e2 : Z,
(0 < m1)%Z ->
(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R ->
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
intros m1 e1 m2 e2 Hp1 (H12, H21).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
assert (He: (e2 < e1)%Z).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
(e2 < e1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
(* . *)
apply Znot_ge_lt.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
~ (e2 >= e1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
intros H0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:(e2 >= e1)%Z
False
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
elim Rlt_not_le with (1 := H21).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:(e2 >= e1)%Z
(F2R {| Fnum := m1 + 1; Fexp := e1 |} <=
 F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
apply Z.ge_le in H0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:(e1 <= e2)%Z
(F2R {| Fnum := m1 + 1; Fexp := e1 |} <=
 F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
apply (F2R_change_exp e1 m2 e2) in H0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:F2R {| Fnum := m2; Fexp := e2 |} =
F2R
  {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
(F2R {| Fnum := m1 + 1; Fexp := e1 |} <=
 F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
rewrite H0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:F2R {| Fnum := m2; Fexp := e2 |} =
F2R
  {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
(F2R {| Fnum := m1 + 1; Fexp := e1 |} <=
 F2R {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
apply F2R_le.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:F2R {| Fnum := m2; Fexp := e2 |} =
F2R
  {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
(m1 + 1 <= m2 * beta ^ (e2 - e1))%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
apply Zlt_le_succ.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:F2R {| Fnum := m2; Fexp := e2 |} =
F2R
  {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
(m1 < m2 * beta ^ (e2 - e1))%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
apply (lt_F2R e1).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
H0:F2R {| Fnum := m2; Fexp := e2 |} =
F2R
  {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |}
(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2 * beta ^ (e2 - e1); Fexp := e1 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
now rewrite <- H0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z /\
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
(* . *)
split.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e2 < e1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
exact He.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(e1 + mag beta (IZR m1))%Z =
(e2 + mag beta (IZR m2))%Z
rewrite (Zplus_comm e1), (Zplus_comm e2).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(mag beta (IZR m1) + e1)%Z =
(mag beta (IZR m2) + e2)%Z
assert (Hp2: (0 < m2)%Z).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(0 < m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
(mag beta (IZR m1) + e1)%Z =
(mag beta (IZR m2) + e2)%Z
apply (gt_0_F2R m2 e2).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(0 < F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
(mag beta (IZR m1) + e1)%Z =
(mag beta (IZR m2) + e2)%Z
apply Rlt_trans with (2 := H12).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
(0 < F2R {| Fnum := m1; Fexp := e1 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
(mag beta (IZR m1) + e1)%Z =
(mag beta (IZR m2) + e2)%Z
now apply F2R_gt_0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
(mag beta (IZR m1) + e1)%Z =
(mag beta (IZR m2) + e2)%Z
rewrite <- 2!mag_F2R.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
mag beta (F2R {| Fnum := m1; Fexp := e1 |}) =
mag beta (F2R {| Fnum := m2; Fexp := e2 |})
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
destruct (mag beta (F2R (Float beta m1 e1))) as (e1', H1).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
Build_mag_prop beta (F2R {| Fnum := m1; Fexp := e1 |})
  e1' H1 = mag beta (F2R {| Fnum := m2; Fexp := e2 |})
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
simpl.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
e1' = mag beta (F2R {| Fnum := m2; Fexp := e2 |})
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply sym_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
mag beta (F2R {| Fnum := m2; Fexp := e2 |}) = e1'
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply mag_unique.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(bpow (e1' - 1) <= F2R {| Fnum := m1; Fexp := e1 |} <
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
rewrite <- (Z.abs_eq m1), F2R_Zabs.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 <= m1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply H1.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
F2R {| Fnum := m1; Fexp := e1 |} <> 0%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 <= m1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply Rgt_not_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(F2R {| Fnum := m1; Fexp := e1 |} > 0)%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 <= m1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply Rlt_gt.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 < F2R {| Fnum := m1; Fexp := e1 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 <= m1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
now apply F2R_gt_0.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
(0 <= m1)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < 
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
now apply Zlt_le_weak.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H1:F2R {| Fnum := m1; Fexp := e1 |} <> 0%R ->
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m1; Fexp := e1 |}) <
 bpow e1')%R
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
clear H1.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <=
 Rabs (F2R {| Fnum := m2; Fexp := e2 |}) < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
rewrite <- F2R_Zabs, Z.abs_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <= F2R {| Fnum := m2; Fexp := e2 |} <
 bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
split.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <= F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(F2R {| Fnum := m2; Fexp := e2 |} < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply Rlt_le.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) < F2R {| Fnum := m2; Fexp := e2 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(F2R {| Fnum := m2; Fexp := e2 |} < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply Rle_lt_trans with (2 := H12).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(bpow (e1' - 1) <= F2R {| Fnum := m1; Fexp := e1 |})%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(F2R {| Fnum := m2; Fexp := e2 |} < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply H2.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(F2R {| Fnum := m2; Fexp := e2 |} < bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply Rlt_le_trans with (1 := H21).beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(F2R {| Fnum := m1 + 1; Fexp := e1 |} <= bpow e1')%R
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
now apply F2R_p1_le_bpow.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
e1':Z
H2:(bpow (e1' - 1) <=
 F2R {| Fnum := m1; Fexp := e1 |} < 
 bpow e1')%R
(0 <= m2)%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
now apply Zlt_le_weak.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m2 <> 0%Z
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply sym_not_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
0%Z <> m2
beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
now apply Zlt_not_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
m1 <> 0%Z
apply sym_not_eq.beta:radix
m1, e1, m2, e2:Z
Hp1:(0 < m1)%Z
H12:(F2R {| Fnum := m1; Fexp := e1 |} <
 F2R {| Fnum := m2; Fexp := e2 |})%R
H21:(F2R {| Fnum := m2; Fexp := e2 |} <
 F2R {| Fnum := m1 + 1; Fexp := e1 |})%R
He:(e2 < e1)%Z
Hp2:(0 < m2)%Z
0%Z <> m1
now apply Zlt_not_eq.
Qed.

End Float_prop.