Library Float.Ct2.FnormI

Require Export FboundI.

Section FboundedI_Def.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.

Theorem LexicoPosCanI :
  (b : FboundI) (x y : float),
 FcanonicI radix b x
 FboundedI b y → (0 x)%R → (x y)%R → (Fexp x Fexp y)%Z.
intros b x y H1 H2 H3 H4.
case H1; intros H5.
case (Zle_or_lt (Fexp x) (Fexp y)); auto; intros H6.
absurd (x y)%R; auto; apply Rlt_not_le.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rle_lt_trans with (vNumSup b × powerRZ radix (Fexp y))%R.
apply Rmult_le_compat_r;
 [ apply powerRZ_le; auto with real zarith
 | rewrite INR_IZR_INZ; apply Rle_IZR; elim H2; intuition ].
apply Rlt_le_trans with (radix × Fnum x × powerRZ radix (Fexp y))%R.
apply Rmult_lt_compat_r; [ apply powerRZ_lt; auto with real zarith | idtac ].
elim H5; intros H9 H7; case H7; auto; intros H8.
absurd (radix × Fnum x < (- vNumInf b)%Z)%R; auto.
apply Rle_not_lt.
apply Rle_trans with (IZR 0); auto with zarith real.
replace (IZR 0) with (radix × 0%Z)%R; auto with real zarith.
apply Rmult_le_compat_l; [ idtac | apply Rle_IZR; apply LeR0Fnum with radix ];
 auto with real zarith arith.
apply Rle_trans with (Fnum x × (radix × powerRZ radix (Fexp y)))%R;
 [ right; ring | idtac ].
apply Rmult_le_compat_l;
 [ replace 0%R with (IZR 0); auto with real zarith; apply Rle_IZR;
    apply LeR0Fnum with radix; auto with arith
 | idtac ].
rewrite <- powerRZ_Zs; auto with real zarith.
apply Rle_powerRZ; auto with real arith zarith.
elim H5; intros H6 H7; elim H7; intros H8 H9.
rewrite H8; elim H2; intuition.
Qed.

Theorem LexicoNegCanI :
  (b : FboundI) (x y : float),
 FcanonicI radix b x
 FboundedI b y → (x 0)%R → (y x)%R → (Fexp x Fexp y)%Z.
intros b x y H1 H2 H3 H4.
case H1; intros H5.
case (Zle_or_lt (Fexp x) (Fexp y)); auto; intros H6.
absurd (y x)%R; auto; apply Rlt_not_le.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite (Zsucc_pred (Fexp x)); rewrite powerRZ_Zs; auto with real zarith.
apply Rlt_le_trans with ((- vNumInf b)%Z × powerRZ radix (Zpred (Fexp x)))%R.
rewrite <- Rmult_assoc; apply Rmult_lt_compat_r; auto with real zarith.
elim H5; intros H9 H7; case H7; intros H8; clear H7.
absurd (vNumSup b < radix × Fnum x)%R; auto; apply Rle_not_lt.
apply Rle_trans with (IZR 0); auto with zarith real.
replace (IZR 0) with (radix × 0%Z)%R; auto with real zarith.
apply Rmult_le_compat_l; [ idtac | apply Rle_IZR; apply R0LeFnum with radix ];
 auto with real zarith arith.
rewrite Rmult_comm; auto with zarith real.
apply Rle_trans with ((- vNumInf b)%Z × powerRZ radix (Fexp y))%R;
 [ idtac | apply Rmult_le_compat_r ]; auto with zarith real.
rewrite Ropp_Ropp_IZR; repeat rewrite Ropp_mult_distr_l_reverse;
 apply Ropp_le_contravar.
apply Rmult_le_compat_l; [ idtac | apply Rle_powerRZ ];
 auto with real arith zarith.
elim H2; intuition.
elim H5; intros H6 H7; elim H7; intros H8 H9.
rewrite H8; elim H2; intuition.
Qed.

Theorem LexicoCanI :
  (b : FboundI) (x y : float),
 Zabs_nat (vNumInf b - vNumSup b) 1 →
 FcanonicI radix b x
 FboundedI b y → (Rabs x < Rabs y)%R → (Fexp x Fexp y)%Z.
intros b x y H1 H2 H3 H4.
case H2; intros H5.
case (Zle_or_lt (Fexp x) (Fexp y)); auto; intros H6.
absurd (Rabs x < Rabs y)%R; auto.
apply Rle_not_lt.
unfold FtoRradix in |- *; repeat rewrite <- Fabs_correct;
 auto with real zarith.
unfold FtoR in |- *; simpl in |- ×.
elim H5; intros H8 H7; case H7; auto; intros H9.
cut (0 < Fnum x)%Z; [ intros H10 | idtac ].
apply Rle_trans with (Zsucc (vNumSup b) × powerRZ radix (Fexp y))%R.
apply Rmult_le_compat_r;
 [ apply powerRZ_le; auto with real zarith | apply Rle_IZR ].
case (Zle_or_lt 0 (Fnum y)); intros H11.
rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (Z_of_nat (vNumSup b));
 [ elim H3; intuition | auto with zarith ].
rewrite Zabs_absolu; rewrite <- absolu_Zopp; auto with zarith.
rewrite inj_abs; auto with zarith.
apply Zle_trans with (Z_of_nat (vNumInf b)); auto with zarith.
rewrite <- (Zopp_involutive (Z_of_nat (vNumInf b))); apply Zle_Zopp;
 elim H3; intuition.
replace (Zsucc (vNumSup b)) with (1%nat + vNumSup b)%Z.
apply le_IZR; rewrite plus_IZR.
apply Rplus_le_reg_l with (- vNumSup b)%R.
apply Rle_trans with (vNumInf b - vNumSup b)%R;
 [ right; rewrite <- INR_IZR_INZ; ring | idtac ].
apply Rle_trans with (INR 1);
 [ idtac | right; repeat rewrite <- INR_IZR_INZ; ring ].
rewrite <- (Rabs_right (vNumSup b)); auto with real arith.
rewrite <- (Rabs_right (vNumInf b)); auto with real arith.
apply Rle_trans with (Rabs (vNumInf b - vNumSup b));
 [ apply Rabs_triang_inv | idtac ].
repeat rewrite INR_IZR_INZ; rewrite Z_R_minus.
rewrite Faux.Rabsolu_Zabs; rewrite Zabs_absolu; auto with arith zarith real.
unfold Zsucc in |- *; auto with arith zarith.
apply Rle_trans with (radix × Fnum x × powerRZ radix (Fexp y))%R.
apply Rmult_le_compat_r; [ apply powerRZ_le; auto with real zarith | idtac ].
repeat rewrite INR_IZR_INZ; rewrite <- Rmult_IZR; apply Rle_IZR.
apply Zlt_le_succ; apply lt_IZR; rewrite Rmult_IZR;
 repeat rewrite <- INR_IZR_INZ; auto with arith zarith real.
apply Rle_trans with (Fnum x × (radix × powerRZ radix (Fexp y)))%R;
 [ right; ring | idtac ].
rewrite Zabs_eq; auto with zarith.
apply Rmult_le_compat_l;
 [ replace 0%R with (IZR 0); auto with real zarith | idtac ].
rewrite <- powerRZ_Zs; auto with real zarith.
apply Rle_powerRZ; auto with real arith zarith.
apply lt_IZR; simpl in |- ×.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rle_lt_trans with 0%R; [ right; ring | idtac ].
apply Rle_lt_trans with (INR (vNumSup b)); auto with arith real.
cut (Fnum x < 0)%Z; [ intros H10 | idtac ].
apply Rle_trans with (Zsucc (vNumInf b) × powerRZ radix (Fexp y))%R.
apply Rmult_le_compat_r;
 [ apply powerRZ_le; auto with real zarith | apply Rle_IZR ].
case (Zle_or_lt 0 (Fnum y)); intros H11.
rewrite Zabs_eq; auto with zarith.
apply Zle_trans with (Z_of_nat (vNumSup b));
 [ elim H3; intuition | auto with zarith ].
replace (Zsucc (vNumInf b)) with (1%nat + vNumInf b)%Z.
apply le_IZR; rewrite plus_IZR.
apply Rplus_le_reg_l with (- vNumInf b)%R.
apply Rle_trans with (vNumSup b - vNumInf b)%R;
 [ right; rewrite <- INR_IZR_INZ; ring | idtac ].
apply Rle_trans with (INR 1);
 [ idtac | right; repeat rewrite <- INR_IZR_INZ; ring ].
rewrite <- (Rabs_right (vNumSup b)); auto with real arith.
rewrite <- (Rabs_right (vNumInf b)); auto with real arith.
apply Rle_trans with (Rabs (vNumSup b - vNumInf b));
 [ apply Rabs_triang_inv | idtac ].
rewrite <- Rabs_Ropp.
replace (- (vNumSup b - vNumInf b))%R with (vNumInf b - vNumSup b)%R;
 [ idtac | ring ].
repeat rewrite INR_IZR_INZ; rewrite Z_R_minus.
rewrite Faux.Rabsolu_Zabs; rewrite Zabs_absolu; auto with arith zarith real.
unfold Zsucc in |- *; auto with arith zarith.
rewrite Zabs_absolu; rewrite <- absolu_Zopp.
rewrite inj_abs; auto with zarith.
apply Zle_trans with (Z_of_nat (vNumInf b)); auto with zarith.
rewrite <- (Zopp_involutive (Z_of_nat (vNumInf b))); apply Zle_Zopp;
 elim H3; intuition.
apply Rle_trans with (radix × (- Fnum x)%Z × powerRZ radix (Fexp y))%R.
apply Rmult_le_compat_r; [ apply powerRZ_le; auto with real zarith | idtac ].
repeat rewrite INR_IZR_INZ; rewrite <- Rmult_IZR; apply Rle_IZR.
apply Zlt_le_succ; apply lt_IZR; rewrite Rmult_IZR;
 repeat rewrite <- INR_IZR_INZ; auto with arith zarith real.
apply Ropp_lt_cancel; rewrite Ropp_Ropp_IZR.
apply Rle_lt_trans with (radix × Fnum x)%R;
 [ right; ring | auto with zarith real ].
rewrite (INR_IZR_INZ (vNumInf b)); rewrite <- Ropp_Ropp_IZR;
 auto with zarith real.
apply Rle_trans with ((- Fnum x)%Z × (radix × powerRZ radix (Fexp y)))%R;
 [ right; ring | idtac ].
rewrite <- (Zabs_eq (- Fnum x)); auto with zarith.
replace (Zabs (- Fnum x)) with (Zabs (Fnum x)); auto with zarith.
apply Rmult_le_compat_l;
 [ replace 0%R with (IZR 0); auto with real zarith | idtac ].
rewrite <- powerRZ_Zs; auto with real zarith.
apply Rle_powerRZ; auto with real arith zarith.
auto with zarith.
repeat rewrite Zabs_absolu; auto with arith zarith.
rewrite absolu_Zopp; auto with zarith arith.
apply lt_IZR; simpl in |- ×.
apply Rmult_lt_reg_l with (IZR radix); auto with real zarith.
apply Rlt_le_trans with 0%R; [ idtac | right; ring ].
apply Rlt_le_trans with (IZR (- vNumInf b)); auto with arith real.
replace 0%R with (IZR (- 0%nat)); auto with real arith zarith.
elim H5; intros H6 H7; elim H7; intros H8 H9.
rewrite H8; elim H3; intuition.
Qed.

Theorem ReductRangeI :
  (b b' : FboundI) (p : nat),
 vNumInf b = vNumInf b'
 dExpI b = dExpI b'
 Z_of_nat (vNumSup b) = (vNumSup b' + 1)%Z
 Z_of_nat (vNumSup b) = (radix × p)%Z
  x : float,
 FboundedI b x y : float, FboundedI b' y x = y :>R.
intros b b' p Hi He Hs1 Hs2 x Fx.
elim Fx; intros H2 H3; elim H2; clear H2; intros H2 H4.
case (Zle_or_lt (Fnum x) (Zpred (vNumSup b))); intros H1.
x; split; auto with real.
repeat (split; auto with zarith arith).
cut (Fnum x = vNumSup b); [ intros H5 | idtac ].
(Float p (Zsucc (Fexp x))); split.
repeat (split; simpl in |- *; auto with zarith arith).
cut (1 p)%Z; [ intros H6 | idtac ].
apply Zle_trans with (p + 0)%Z; auto with zarith arith.
apply Zle_trans with (p + (p - 1))%Z; auto with zarith arith.
apply Zle_trans with (2 × p - 1)%Z; auto with zarith arith.
apply Zle_trans with (radix × p - 1)%Z; auto with zarith arith.
unfold Zminus in |- *; apply Zplus_le_compat_r.
apply Zmult_le_compat_r; auto with zarith arith.
CaseEq p; auto with zarith arith; intros H6.
absurd (Z_of_nat (vNumSup b) = 0%Z); auto with zarith arith.
rewrite Hs2; rewrite H6; ring.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *;
 rewrite powerRZ_Zs; auto with zarith real.
rewrite H5; rewrite Hs2; ring_simplify; rewrite mult_IZR; ring.
apply Zle_antisym; auto with zarith.
Qed.

Theorem ReductRangeIInv :
  b b' : FboundI,
 vNumInf b = vNumInf b'
 dExpI b = dExpI b'
 Z_of_nat (vNumSup b) = (vNumSup b' + 1)%Z
 ( x : float,
  FboundedI b x y : float, FboundedI b' y FtoRradix x = y) →
  p : Z, Z_of_nat (vNumSup b) = (radix × p)%Z.
intros b b' Hi He Hs H1.
elim (H1 (Float (vNumSup b) 0));
 [ intros y E; elim E; intros H'1 H'2; clear E | idtac ].
2: repeat split; simpl in |- *; auto with zarith.
cut (INR (vNumSup b) = FtoRradix y);
 [ intros H'3
 | rewrite <- H'2; unfold FtoRradix, FtoR in |- *; simpl in |- *;
    rewrite <- INR_IZR_INZ; ring ].
cut (0 Zpred (Fexp y))%Z; [ intros H3 | idtac ].
(Fnum y × Zpower_nat radix (Zabs_nat (Zpred (Fexp y))))%Z.
cut ( a b : Z, IZR a = IZR ba = b);
 [ intros H4; apply H4 | idtac ].
repeat rewrite Rmult_IZR; repeat rewrite <- INR_IZR_INZ.
rewrite Zpower_nat_powerRZ_absolu; auto with zarith arith; rewrite H'3.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *;
 unfold Zpred in |- ×.
apply trans_eq with (Fnum y × (radix × powerRZ radix (Fexp y + -1)))%R.
pattern (IZR radix) at 2 in |- *; replace (IZR radix) with (powerRZ radix 1);
 [ rewrite <- powerRZ_add | simpl in |- × ]; auto with real zarith.
replace (1 + (Fexp y + -1))%Z with (Fexp y); ring.
repeat rewrite <- INR_IZR_INZ; ring.
intros u v Hw; apply Zplus_reg_l with (- v)%Z.
replace (- v + v)%Z with 0%Z; [ apply IZR_zero_r | ring ].
rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real.
rewrite Hw; ring.
apply Zlt_succ_le; rewrite <- Zsucc_pred.
case (Zle_or_lt (Fexp y) 0); intros H3; auto.
absurd (vNumSup b vNumSup b - 1)%Z; auto with arith zarith.
apply le_IZR; rewrite <- INR_IZR_INZ; rewrite H'3.
rewrite Hs; ring_simplify (vNumSup b' + 1 - 1)%Z; unfold FtoRradix, FtoR in |- *;
 simpl in |- ×.
apply Rle_trans with (Fnum y × powerRZ radix 0)%R.
apply Rmult_le_compat_l;
 [ idtac | apply Rle_powerRZ; auto with real arith zarith ].
replace 0%R with (IZR 0); auto with real; apply Rle_IZR.
apply LeR0Fnum with radix; auto; fold FtoRradix in |- *; rewrite <- H'3;
 auto with zarith real.
simpl in |- *; ring_simplify; elim H'1; intros H4 H5; elim H4;
 auto with zarith real.
Qed.

End FboundedI_Def.

Section FroundI.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : FboundI.
Hypothesis vNumSupGreaterThanOne : (1 vNumSup b)%Z.
Hypothesis vNumInfGreaterThanOne : (1 vNumInf b)%Z.

Definition isMinI (r : R) (min : float) :=
  FboundedI b min
  (min r)%R
  ( f : float, FboundedI b f → (f r)%R → (f min)%R).

Definition isMaxI (r : R) (max : float) :=
  FboundedI b max
  (r max)%R
  ( f : float, FboundedI b f → (r f)%R → (max f)%R).

Definition ProjectorPI (P : RfloatProp) :=
   p q : float, FboundedI b pP p qp = q :>R.

Definition MonotonePI (P : RfloatProp) :=
   (p q : R) (p' q' : float),
  (p < q)%RP p p'P q q' → (p' q')%R.

Definition TotalPI (P : RfloatProp) :=
   r : R, p : float, P r p.

Definition CompatiblePI (P : RfloatProp) :=
   (r1 r2 : R) (p q : float),
  P r1 pr1 = r2p = q :>RFboundedI b qP r2 q.

Definition MinOrMaxPI (P : RfloatProp) :=
   (r : R) (p : float), P r pisMinI r p isMaxI r p.

Definition RoundedModePI (P : RfloatProp) :=
  TotalPI P CompatiblePI P MinOrMaxPI P MonotonePI P.

Theorem ProjectMinI : ProjectorPI isMinI.
red in |- ×.
intros p q H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
 auto with real.
elim H'0; intros H'1 H'2; elim H'2; auto with real.
Qed.

Theorem ProjectMaxI : ProjectorPI isMaxI.
red in |- ×.
intros p q H' H'0; apply Rle_antisym.
elim H'0; intros H'1 H'2; elim H'2; auto with real.
elim H'0; intros H'1 H'2; elim H'2; intros H'3 H'4; apply H'4; clear H'2;
 auto with real.
Qed.

Theorem RoundedProjectorI : P, RoundedModePI PProjectorPI P.
intros P H'; red in |- *; simpl in |- ×.
intros p q H'0 H'1.
red in H'.
elim H'; intros H'2 H'3; elim H'3; intros H'4 H'5; elim H'5; intros H'6 H'7;
 case (H'6 p q); clear H'5 H'3 H'; auto.
intros H'; apply (ProjectMinI p); auto.
intros H'; apply (ProjectMaxI p); auto.
Qed.

Theorem RoundedModeProjectorIdemI :
  P (p : float), RoundedModePI PFboundedI b pP p p.
intros P p H' H.
elim H'; intros H'0 H'1; elim H'1; intros H'2 H'3; elim H'3; intros H'4 H'5;
 clear H'3 H'1.
case (H'0 p).
intros x H'6.
apply (H'2 p p x); auto.
apply sym_eq; apply (RoundedProjectorI P H'); auto.
Qed.

Theorem OppositeIUnique_1 :
  (x y z : float) P,
 RoundedModePI P
 FboundedI b x
 FboundedI b y
 (- x < y)%RP (x + y)%R z → (powerRZ radix (- dExpI b) z)%R.
intros x y z P HP Fx Fy H1 H2.
cut (powerRZ radix (- dExpI b) = Float 1 (- dExpI b));
 [ intros V; rewrite V
 | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
cut (powerRZ radix (- dExpI b) x + y)%R;
 [ intros H'; case H'; clear H'; intros H' | idtac ].
red in HP; elim HP; intros HP1 tmp; elim tmp; intros HP2 tmp2; elim tmp2;
 intros HP3 HP4; clear tmp tmp2.
apply HP4 with (powerRZ radix (- dExpI b)) (x + y)%R; auto.
rewrite V; apply RoundedModeProjectorIdemI; auto.
repeat (split; simpl in |- *; auto with zarith).
cut (ProjectorPI P); [ intros HP' | apply RoundedProjectorI; auto ].
right; apply HP'; auto.
repeat (split; simpl in |- *; auto with zarith).
rewrite <- V; rewrite H'; auto.
unfold FtoRradix in |- *; rewrite <- Fplus_correct; auto with zarith.
apply Rle_trans with (1%Z × powerRZ radix (- dExpI b))%R;
 [ right; simpl; ring | idtac ].
unfold FtoR in |- *; simpl in |- ×.
apply Rle_trans with (1 × powerRZ radix (Zmin (Fexp x) (Fexp y)))%R.
apply Rmult_le_compat_l; auto with real; apply Rle_powerRZ;
 auto with zarith real.
apply Zmin_Zle; [ elim Fx | elim Fy ]; auto.
apply Rmult_le_compat_r; auto with real zarith.
cut ( k : Z, (0 < k)%Z → (1 k)%R); auto with real zarith;
 intros V'; apply V'.
replace
 (Fnum x × Zpower_nat radix (Zabs_nat (Fexp x - Zmin (Fexp x) (Fexp y))) +
  Fnum y × Zpower_nat radix (Zabs_nat (Fexp y - Zmin (Fexp x) (Fexp y))))%Z
 with (Fnum (Fplus radix x y)); [ apply LtR0Fnum with radix | simpl in |- × ];
 auto.
rewrite Fplus_correct; auto with zarith real;
 apply Rplus_lt_reg_r with (- FtoR radix x)%R.
ring_simplify; auto.
Qed.

Theorem OppositeIUnique_2 :
  (x y z : float) P,
 RoundedModePI P
 FboundedI b x
 FboundedI b y
 (y < - x)%RP (x + y)%R z → (powerRZ radix (- dExpI b) - z)%R.
intros x y z P HP Fx Fy H1 H2.
apply Ropp_le_cancel; rewrite Ropp_involutive.
cut ((- powerRZ radix (- dExpI b))%R = Float (-1) (- dExpI b));
 [ intros V; rewrite V
 | unfold FtoRradix, FtoR in |- *; simpl in |- *; ring ].
cut (x + y - powerRZ radix (- dExpI b))%R;
 [ intros H'; case H'; clear H'; intros H' | idtac ].
red in HP; elim HP; intros HP1 tmp; elim tmp; intros HP2 tmp2; elim tmp2;
 intros HP3 HP4; clear tmp tmp2.
apply HP4 with (x + y)%R (- powerRZ radix (- dExpI b))%R; auto.
rewrite V; apply RoundedModeProjectorIdemI; auto.
repeat (split; simpl in |- *; auto with zarith).
cut (ProjectorPI P); [ intros HP' | apply RoundedProjectorI; auto ].
right; apply sym_eq; apply HP'; auto.
repeat (split; simpl in |- *; auto with zarith).
rewrite <- V; rewrite <- H'; auto.
unfold FtoRradix in |- *; rewrite <- Fplus_correct; auto with zarith.
apply Rle_trans with ((-1)%Z × powerRZ radix (- dExpI b))%R;
 [ idtac | right; auto with real zarith ].
unfold FtoR in |- *; simpl in |- ×.
apply Rle_trans with (-1 × powerRZ radix (Zmin (Fexp x) (Fexp y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Ropp_le_cancel; rewrite Ropp_involutive.
cut ( k : Z, (0 < - k)%Z → (1 - k)%R); auto with real zarith.
intros V'; apply V'.
replace
 (-
  (Fnum x × Zpower_nat radix (Zabs_nat (Fexp x - Zmin (Fexp x) (Fexp y))) +
   Fnum y × Zpower_nat radix (Zabs_nat (Fexp y - Zmin (Fexp x) (Fexp y)))))%Z
 with (Fnum (Fopp (Fplus radix x y)));
 [ apply LtR0Fnum with radix | simpl in |- × ]; auto.
rewrite Fopp_correct; rewrite Fplus_correct; auto with zarith real;
 apply Rplus_lt_reg_r with (FtoR radix y).
ring_simplify; auto.
intros k; replace (- k)%R with (IZR (- k)); auto with zarith real;
 apply Ropp_Ropp_IZR.
apply Ropp_le_cancel; ring_simplify.
apply Rle_powerRZ; auto with zarith real; apply Zmin_Zle;
 [ elim Fx | elim Fy ]; auto.
Qed.

Theorem OppositeIUnique :
  (x y z : float) P,
 RoundedModePI P
 FboundedI b x
 FboundedI b y
 (- x)%R yP (x + y)%R z → (powerRZ radix (- dExpI b) Rabs z)%R.
intros x y z P HP Fx Fy H1 H2.
case (Rle_or_lt (- x) y); intros H3; [ case H3; intros H4 | idtac ].
apply Rle_trans with (FtoRradix z); [ idtac | apply RRle_abs ].
apply OppositeIUnique_1 with x y P; auto.
absurd ((- FtoRradix x)%R = FtoRradix y); auto with real.
rewrite <- Rabs_Ropp; apply Rle_trans with (- FtoRradix z)%R;
 [ idtac | apply RRle_abs ].
apply OppositeIUnique_2 with x y P; auto.
Qed.

End FroundI.

Section FpropI.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variable b : FboundI.

Theorem SterbenzIAux1 :
  x y : float,
 FboundedI b x
 FboundedI b y
 (y x)%R → (x 2%nat × y)%RFboundedI b (Fminus radix x y).
intros x y H' H'0 H'1 H'2.
cut (0 Fminus radix x y)%R; [ intros Rle1 | idtac ].
cut (Fminus radix x y y)%R; [ intros Rle2 | idtac ].
case (Zle_or_lt (Fexp x) (Fexp y)); intros Zle1.
repeat split.
apply Zle_trans with 0%Z; auto with zarith.
apply (LeR0Fnum radix); auto.
apply Zle_trans with (Fnum x).
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
apply Rle_trans with (2 := H'1); auto.
unfold Fminus in |- *; simpl in |- *; apply Zmin_le1; auto.
elim H'; intuition.
unfold Fminus in |- *; simpl in |- *; rewrite Zmin_le1; auto.
elim H'; intuition.
repeat split.
apply Zle_trans with 0%Z; auto with zarith.
apply (LeR0Fnum radix); auto.
apply Zle_trans with (Fnum y).
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
unfold Fminus in |- *; simpl in |- *; apply Zmin_le2; auto with zarith.
elim H'0; intuition.
unfold Fminus in |- *; simpl in |- *; rewrite Zmin_le2; auto with zarith.
elim H'0; intuition.
rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- ×.
apply Rplus_le_reg_l with (r := FtoRradix y); auto with real.
replace (y + (x - y))%R with (FtoRradix x); [ idtac | ring ].
replace (y + y)%R with (2%nat × y)%R; [ auto | simpl in |- *; ring ].
rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- ×.
apply Rplus_le_reg_l with (r := FtoRradix y); auto with real.
replace (y + (x - y))%R with (FtoRradix x); [ auto with real | ring ].
replace (y + 0)%R with (FtoRradix y); [ auto | simpl in |- *; ring ].
Qed.

Theorem SterbenzOppI :
  x y : float,
 ( u : float, FboundedI b u
     v : float, FtoRradix v = (- u)%R FboundedI b v) →
 FboundedI b xFboundedI b y
 (/ 2%nat × y x)%R → (x 2%nat × y)%R
  z : float,
   FtoRradix z = (x - y)%R FboundedI b z.
intros x y H1 Fx Fy H2 H3.
case (Rle_or_lt y x); intros H4.
(Fminus radix x y); split; auto with float real.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
apply SterbenzIAux1; auto.
cut
 (ex
    (fun v : float
     FtoRradix v = (- FtoRradix (Fminus radix y x))%R FboundedI b v));
 [ intros H5; elim H5; intros v H6 | apply H1 ].
elim H6; clear H5 H6; intros H5 H6; v; split; auto.
rewrite H5; unfold FtoRradix in |- *; rewrite Fminus_correct;
 auto with zarith real.
apply SterbenzIAux1; auto with real.
apply Rmult_le_reg_l with (/ 2%nat)%R; auto with real arith.
apply Rle_trans with (1 := H2); right; field; auto with real arith.
Qed.

Theorem FoppBoundedI :
  (b : FboundI) (x : float) (m : nat),
 Z_of_nat (vNumSup b) = (radix × m - 1%nat)%Z
 Z_of_nat (vNumInf b) = (radix × m)%Z
 FboundedI b x
  y : float,
   FtoRradix y = (- x)%R FboundedI b y.
intros b0 x p H1 H2 Hx.
cut (1 p); [ intros Hp | idtac ].
case (Zle_or_lt (- vNumInf b0) (Fnum x)); intros H3.
2: absurd (Fnum x < Fnum x)%Z; auto with zarith.
2: elim Hx; intuition; auto with zarith.
cut ( a b : Z, (a b)%Za = b (a < b)%Z);
 [ intros F | idtac ].
2: intros a c V; omega.
lapply (F (- vNumInf b0)%Z (Fnum x)); [ intros H'1 | auto ].
case H'1; intros H'2; clear H'1 F.
(Float p (Zsucc (Fexp x))).
repeat split.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite <- H'2; rewrite H2; rewrite Ropp_Ropp_IZR.
ring_simplify; unfold Zsucc in |- *; repeat rewrite <- INR_IZR_INZ.
rewrite powerRZ_add; auto with zarith real; simpl in |- ×.
rewrite Rmult_IZR; repeat rewrite <- INR_IZR_INZ; ring.
simpl in |- *; apply Zle_trans with 0%Z; auto with arith zarith.
simpl in |- *; rewrite H1.
apply Zle_trans with (p + p - 1%nat)%Z.
apply Zplus_le_reg_l with (- p + 1%nat)%Z.
replace (- p + 1%nat + p)%Z with (Z_of_nat 1); [ idtac | ring ].
replace (- p + 1%nat + (p + p - 1%nat))%Z with (Z_of_nat p); [ idtac | ring ];
 auto with arith zarith.
replace (p + p)%Z with (2%nat × p)%Z; unfold Zminus in |- *;
 auto with arith zarith.
apply Zplus_le_compat_r; apply Zle_Zmult_comp_r; auto with arith zarith.
replace (Z_of_nat 2) with 2%Z; auto with arith zarith.
replace (Z_of_nat 2) with 2%Z; auto with arith zarith.
simpl in |- *; apply Zle_trans with (Fexp x); auto with zarith; elim Hx;
 intuition.
(Fopp x).
repeat split; auto with real float arith zarith.
unfold FtoRradix in |- *; apply Fopp_correct; auto.
simpl in |- *; apply Zle_Zopp.
apply Zle_trans with (Z_of_nat (vNumSup b0)); auto with zarith.
elim Hx; intuition.
simpl in |- *; rewrite <- (Zopp_involutive (vNumSup b0));
 apply Zle_Zopp.
apply Zlt_succ_le.
replace (- vNumSup b0)%Z with (Zsucc (- vNumInf b0)).
apply Zsucc_lt_compat; auto.
rewrite H2; rewrite H1; rewrite <- Zopp_Zpred_Zs; auto with zarith.
simpl in |- *; elim Hx; intuition.
CaseEq p; auto with arith zarith.
intros Hp; generalize H1; rewrite Hp; simpl in |- ×.
replace (radix × 0 - 1)%Z with (-1)%Z; [ auto with arith zarith | ring ].
Qed.

Theorem FoppBoundedI2 :
  (b0 : FboundI) (x : float) (p : nat),
 Z_of_nat (vNumInf b0) = (radix × p - 1%nat)%Z
 Z_of_nat (vNumSup b0) = (radix × p)%Z
 FboundedI b0 x y : float, FtoRradix y = (- x)%R FboundedI b0 y.
intros b0 x p H1 H2 H3.
elim
 FoppBoundedI with (BoundI (vNumSup b0) (vNumInf b0) (dExpI b0)) (Fopp x) p;
 auto.
intros u tmp; elim tmp; intros H4 H5; clear tmp; (Fopp u); split.
unfold FtoRradix in |- *; rewrite Fopp_correct; fold FtoRradix in |- *;
 rewrite H4; unfold FtoRradix in |- *; rewrite Fopp_correct;
 ring.
elim H5; simpl in |- *; intros tmp H6; elim tmp; intros H7 H8; clear tmp;
 split; auto with zarith.
unfold Fopp in |- *; simpl in |- *; split; auto with zarith.
elim H3; simpl in |- *; intros tmp H6; elim tmp; intros H7 H8; clear tmp;
 split; auto with zarith.
unfold Fopp in |- *; simpl in |- *; split; auto with zarith.
Qed.

Theorem FoppBoundedIInv_aux :
  n : Z,
 (vNumSup b + 1%nat - n)%Z
 (- n vNumInf b)%Z
 ( x : float,
  FboundedI b x y : float, FtoRradix y = (- x)%R FboundedI b y) →
  p : Z, n = (radix × p)%Z.
intros n H1 H2 H.
elim (H (Float n 0)); [ intros y E; elim E; intros H'1 H'2; clear E | idtac ].
2: repeat split; simpl in |- *; auto with zarith.
cut (0 Zpred (Fexp y))%Z; [ intros H3 | idtac ].
(- (Fnum y × Zpower_nat radix (Zabs_nat (Zpred (Fexp y)))))%Z.
cut ( a b : Z, IZR a = IZR ba = b);
 [ intros H4; apply H4 | idtac ].
rewrite Rmult_IZR; rewrite Ropp_Ropp_IZR; rewrite Rmult_IZR.
repeat rewrite <- INR_IZR_INZ.
rewrite Zpower_nat_powerRZ_absolu; auto with zarith arith.
replace (IZR n) with (- y)%R.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *;
 unfold Zpred in |- ×.
apply trans_eq with (- (Fnum y × (radix × powerRZ radix (Fexp y + -1))))%R.
pattern (IZR radix) at 2 in |- *; replace (IZR radix) with (powerRZ radix 1);
 [ rewrite <- powerRZ_add | simpl in |- × ]; auto with real zarith.
replace (1 + (Fexp y + -1))%Z with (Fexp y); ring.
repeat rewrite <- INR_IZR_INZ; ring.
replace (IZR n) with (FtoRradix (Float n 0)); auto with real float.
rewrite H'1; rewrite Ropp_involutive; auto with real.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *; ring.
intros u v Hw; apply Zplus_reg_l with (- v)%Z.
replace (- v + v)%Z with 0%Z; [ apply IZR_zero_r | ring ].
rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real.
rewrite Hw; ring.
apply Zlt_succ_le; rewrite <- Zsucc_pred.
case (Zle_or_lt (Fexp y) 0); intros H3; auto.
absurd (vNumSup b + 1%nat vNumSup b)%Z.
rewrite <- inj_plus; auto with arith zarith.
apply Zle_trans with (- n)%Z; auto.
apply le_IZR; rewrite Ropp_Ropp_IZR.
replace (IZR n) with (FtoRradix (Float n 0));
 [ idtac
 | unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *; ring ].
rewrite <- H'1; unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
apply Rle_trans with (IZR (Fnum y));
 [ idtac | elim H'2; intuition; auto with real ].
apply Rle_trans with (Fnum y × powerRZ radix 0)%R;
 [ idtac | simpl in |- *; right; ring ].
apply Rmult_le_compat_l;
 [ idtac | apply Rle_powerRZ; auto; apply Rlt_le; auto with real arith ].
replace 0%R with (IZR 0); auto with real; apply Rle_IZR.
apply LeR0Fnum with radix; auto; fold FtoRradix in |- ×.
replace (FtoRradix y) with (IZR (- n)); auto with arith zarith.
replace 0%R with (IZR 0); auto with arith zarith real.
rewrite Ropp_Ropp_IZR.
replace (IZR n) with (FtoRradix (Float n 0));
 [ auto
 | unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *; ring ].
Qed.

Theorem FoppBoundedIExp :
  (x : float) (p : nat),
 Z_of_nat (vNumSup b) = (radix × p - 1%nat)%Z
 Z_of_nat (vNumInf b) = (radix × p)%Z
 FboundedI b x
  y : float,
   FtoRradix y = (- x)%R
   FboundedI b y (Fexp y = Fexp x Fexp y = Zsucc (Fexp x)).
intros x p H1 H2 Hx.
cut (1 p); [ intros Hp | idtac ].
case (Zle_or_lt (- vNumInf b) (Fnum x)); intros H3.
2: absurd (Fnum x < Fnum x)%Z; auto with zarith.
2: elim Hx; intuition; auto with zarith.
cut ( a b : Z, (a b)%Za = b (a < b)%Z);
 [ intros F | idtac ].
2: intros a c V; omega.
lapply (F (- vNumInf b)%Z (Fnum x)); [ intros H'1 | auto ].
case H'1; intros H'2; clear H'1 F.
(Float p (Zsucc (Fexp x))).
repeat split.
unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- ×.
rewrite <- H'2; rewrite H2; rewrite Ropp_Ropp_IZR.
ring_simplify; unfold Zsucc in |- *; repeat rewrite <- INR_IZR_INZ.
rewrite powerRZ_add; auto with zarith real; simpl in |- ×.
rewrite Rmult_IZR; repeat rewrite <- INR_IZR_INZ; ring.
simpl in |- *; apply Zle_trans with 0%Z; auto with arith zarith.
simpl in |- *; rewrite H1.
apply Zle_trans with (p + p - 1%nat)%Z.
apply Zplus_le_reg_l with (- p + 1%nat)%Z.
replace (- p + 1%nat + p)%Z with (Z_of_nat 1); [ idtac | ring ].
replace (- p + 1%nat + (p + p - 1%nat))%Z with (Z_of_nat p); [ idtac | ring ];
 auto with arith zarith.
replace (p + p)%Z with (2%nat × p)%Z; unfold Zminus in |- *;
 auto with arith zarith.
apply Zplus_le_compat_r; apply Zle_Zmult_comp_r; auto with arith zarith.
replace (Z_of_nat 2) with 2%Z; auto with arith zarith.
replace (Z_of_nat 2) with 2%Z; auto with arith zarith.
simpl in |- *; apply Zle_trans with (Fexp x); auto with zarith; elim Hx;
 intuition.
simpl in |- *; auto with zarith.
(Fopp x).
repeat split; auto with real float arith zarith.
unfold FtoRradix in |- *; apply Fopp_correct; auto.
simpl in |- *; apply Zle_Zopp.
apply Zle_trans with (Z_of_nat (vNumSup b)); auto with zarith.
elim Hx; intuition.
simpl in |- *; rewrite <- (Zopp_involutive (vNumSup b));
 apply Zle_Zopp.
apply Zlt_succ_le.
replace (- vNumSup b)%Z with (Zsucc (- vNumInf b)).
apply Zsucc_lt_compat; auto.
rewrite H2; rewrite H1; rewrite <- Zopp_Zpred_Zs; auto with zarith.
simpl in |- *; elim Hx; intuition.
CaseEq p; auto with arith zarith.
intros Hp; generalize H1; rewrite Hp; simpl in |- ×.
replace (radix × 0 - 1)%Z with (-1)%Z; [ auto with arith zarith | ring ].
Qed.

Theorem nat_div_one : n m : nat, m × n = 1 → m = 1.
intros n m; case m; case n; simpl in |- *; auto with arith.
intros n'; rewrite mult_comm; simpl in |- *; intros; discriminate.
intros n' n''; case n''; simpl in |- *; auto with arith.
intros n0;
 replace (S (n' + S (n' + n0 × S n'))) with (S (S (n' + (n' + n0 × S n'))));
 auto with arith.
intros; discriminate.
Qed.

Theorem Z_div_one :
  (n : nat) (z : Z), (z × Z_of_nat n)%Z = Z_of_nat 1 → n = 1.
intros n z H.
cut (0 < n); [ intros L1 | idtac ].
apply (nat_div_one (Zabs_nat z)).
apply inject_nat_eq; rewrite inj_mult; rewrite inj_abs.
rewrite Zmult_comm; auto with arith.
apply le_IZR; apply Rmult_le_reg_l with (IZR (Z_of_nat n));
 repeat rewrite <- Rmult_IZR; auto with real arith zarith.
replace (n × 0)%Z with (Z_of_nat 0); auto with zarith arith.
rewrite Zmult_comm; apply Rle_IZR; rewrite H; auto with zarith arith.
replace (Z_of_nat 0) with 0%Z; auto with zarith arith.
generalize H; case n; simpl in |- *; auto with zarith arith.
Qed.

Theorem FoppBoundedIInv :
 (vNumSup b < vNumInf b)%Z
 ( x : float, FboundedI b x
      y : float, FtoRradix y = (- x)%R FboundedI b y) →
 ( m : Z,
   Z_of_nat (vNumInf b) = (radix × m)%Z)
   Z_of_nat (vNumInf b) = (vNumSup b + 1%nat)%Z.
intros H1 H2.
generalize FoppBoundedIInv_aux; intros H3.
elim (H3 (- (vNumSup b + 1%nat))%Z); [ intros p E | idtac | idtac | idtac ];
 auto with zarith.
2: rewrite Zopp_involutive; auto with zarith arith.
2: replace (vNumSup b + 1%nat)%Z with (Zsucc (vNumSup b));
    auto with zarith arith.
case (Zle_or_lt (vNumInf b) (vNumSup b + 1%nat)); intros H4.
cut (Z_of_nat (vNumInf b) = (vNumSup b + 1%nat)%Z); [ intros H5 | idtac ].
2: apply Zeq_Zs; auto with zarith arith.
2: replace (vNumSup b + 1%nat)%Z with (Zsucc (vNumSup b));
    auto with zarith arith.
repeat split; auto with zarith.
(- p)%Z; rewrite H5.
replace (radix × - p)%Z with (- (radix × p))%Z; [ rewrite <- E | idtac ];
 ring.
elim (H3 (- (vNumSup b + 2%nat))%Z); [ intros p0 E0 | idtac | idtac | idtac ];
 auto with zarith.
2: rewrite Zopp_involutive; apply Zplus_le_compat_l;
    auto with zarith arith.
2: rewrite Zopp_involutive;
    replace (vNumSup b + 2%nat)%Z with (Zsucc (vNumSup b + 1%nat));
    [ apply Zlt_le_succ | idtac ]; auto with zarith arith.
2: replace (vNumSup b + 2%nat)%Z with (vNumSup b + (1%nat + 1%nat))%Z;
    auto with zarith arith.
2: replace (vNumSup b + (1%nat + 1%nat))%Z with (vNumSup b + 1%nat + 1%nat)%Z;
    auto with zarith arith.
absurd (Z_of_nat 1 = Zabs_nat radix); auto with arith zarith.
apply Zlt_not_eq; auto with arith zarith.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with arith zarith.
cut
 ( n : nat,
  ( p : Z, Z_of_nat 1 = (p × n)%Z) → Z_of_nat 1 = n);
 [ intros H5 | idtac ].
apply H5; auto; (p - p0)%Z.
rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with arith zarith.
apply trans_eq with (radix×p-radix×p0)%Z; try ring.
rewrite <- E0; rewrite <- E; ring.
intros n V; elim V; intros r W.
apply sym_eq; apply inj_eq; apply Z_div_one with r; auto with arith.
Qed.

Theorem SterbenzIAux2A :
  (x y : float) (n : nat),
 Zabs_nat (vNumInf b - vNumSup b) n
 FboundedI b x
 FboundedI b y
 (Fexp y Fexp x)%Z
 (y x)%R
 (x 2%nat × y - n × powerRZ radix (Fexp y))%R
 (Fminus radix y x 0)%R
 (- vNumInf b - vNumSup b + n)%ZFboundedI b (Fminus radix y x).
intros x y n H H' H'0 Zle2 H'1 H'2 Rle1 Zle1.
repeat split.
apply Zle_trans with (- vNumSup b + n)%Z; auto with zarith.
apply Zle_trans with (- Fnum y + n)%Z; auto with zarith.
apply Zplus_le_compat_r; apply Zle_Zopp; unfold FboundedI in H'0; intuition.
replace (- Fnum y + n)%Z with
 (Fnum (Fplus radix (Fopp y) (Float n (Fexp y)))).
apply Rle_Fexp_eq_Zle with (radix := radix); auto with arith.
rewrite Fminus_correct; auto with zarith; rewrite Fplus_correct;
 auto with zarith; rewrite Fopp_correct.
apply
 Rplus_le_reg_l
  with (x + - (- FtoR radix y + FtoR radix (Float n (Fexp y))))%R.
replace
 (x + - (- FtoR radix y + FtoR radix (Float n (Fexp y))) +
  (- FtoR radix y + FtoR radix (Float n (Fexp y))))%R with (
 FtoRradix x); [ idtac | ring ].
replace
 (x + - (- FtoR radix y + FtoR radix (Float n (Fexp y))) +
  (FtoR radix y - FtoR radix x))%R with (2%nat × y - Float n (Fexp y))%R.
replace (FtoRradix (Float n (Fexp y))) with (n × powerRZ radix (Fexp y))%R; auto.
unfold FtoRradix, FtoR; simpl; rewrite <- INR_IZR_INZ; auto with real.
replace (2%nat × y)%R with (y + y)%R; unfold FtoRradix in |- *;
 [ ring; ring | simpl in |- *; ring ].
unfold Fminus in |- *; simpl in |- *; repeat rewrite Zmin_le1;
 auto with zarith.
unfold Fplus in |- *; simpl in |- ×.
repeat rewrite Zmin_le1; auto with zarith; simpl in |- ×.
replace (Zabs_nat (Fexp y - Fexp y)) with 0; auto with zarith.
unfold Zpower_nat in |- *; simpl in |- *; ring.
replace (Fexp y - Fexp y)%Z with 0%Z; auto with arith zarith.
apply Zle_trans with 0%Z; auto with zarith.
rewrite <- (Zopp_involutive (Fnum (Fminus radix y x))).
replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp.
replace (- Fnum (Fminus radix y x))%Z with (Fnum (Fopp (Fminus radix y x)));
 [ idtac | unfold Fopp in |- *; simpl in |- × ].
apply (LeR0Fnum radix); auto.
rewrite Fopp_correct.
replace 0%R with (-0)%R; auto with real; apply Ropp_le_ge_contravar.
ring.
unfold Fminus in |- *; simpl in |- ×.
rewrite Zmin_le1; auto with zarith.
elim H'0; intuition.
Qed.

Theorem SterbenzIAux2B :
  (x y : float) (n : nat),
 Zabs_nat (vNumInf b - vNumSup b) n
 FboundedI b x
 FboundedI b y
 (Fexp x Fexp y)%Z
 (y 0)%R
 (y x)%R
 (x 2%nat × y - n × powerRZ radix (Fexp x))%R
 (Fminus radix y x 0)%R
 (- vNumInf b - vNumSup b + n)%ZFboundedI b (Fminus radix y x).
intros x y n H H' H'0 Zle2 H'1 H'2 Rle1 Zle1 G.
repeat split.
apply Zle_trans with (- vNumSup b + n)%Z; auto with zarith.
apply Zle_trans with (- Fnum y + n)%Z; auto with zarith.
apply Zplus_le_compat_r; apply Zle_Zopp; unfold FboundedI in H'0; intuition.
apply
 Zle_trans
  with (- Fnum y × Zpower_nat radix (Zabs_nat (Fexp y - Fexp x)) + n)%Z.
apply Zplus_le_compat_r.
pattern (- Fnum y)%Z at 1 in |- *;
 replace (- Fnum y)%Z with (- Fnum y × Zpower_nat radix 0)%Z.
2: unfold Zpower_nat in |- *; simpl in |- *; auto with arith zarith.
apply Zle_Zmult_comp_l.
replace (- Fnum y)%Z with (Fnum (Fopp y)); auto with float.
apply LeR0Fnum with radix; auto with float real.
rewrite Fopp_correct; auto with float real.
apply le_IZR.
rewrite Zpower_nat_powerRZ_absolu; auto with zarith.
rewrite Zpower_nat_Z_powerRZ; auto with zarith real.
apply Rle_powerRZ; auto with real zarith.
apply le_IZR; rewrite plus_IZR; rewrite Rmult_IZR; rewrite Ropp_Ropp_IZR.
rewrite Zpower_nat_powerRZ_absolu; auto with zarith.
apply Rle_monotony_contra_exp with radix (Fexp x); auto.
apply
 Rle_trans
  with
    (- Fnum y × (powerRZ radix (Fexp y - Fexp x) × powerRZ radix (Fexp x)) +
     powerRZ radix (Fexp x) × n)%R;
 [ right; repeat rewrite <- INR_IZR_INZ; ring | idtac ].
rewrite <- powerRZ_add; auto with real zarith.
replace (Fexp y - Fexp x + Fexp x)%Z with (Fexp y); [ idtac | ring ].
replace (- Fnum y × powerRZ radix (Fexp y))%R with (- y)%R;
 [ idtac
 | unfold FtoRradix in |- *; unfold FtoR in |- *; simpl in |- *; ring ].
replace (Fnum (Fminus radix y x) × powerRZ radix (Fexp x))%R with (y - x)%R.
apply Rplus_le_reg_l with (y + x + - (n × powerRZ radix (Fexp x)))%R.
apply Rle_trans with (FtoRradix x); [ right; ring | idtac ].
apply Rle_trans with (y + y - n × powerRZ radix (Fexp x))%R;
 [ idtac | right; ring ].
replace (y + y)%R with (2%nat × y)%R; [ auto | simpl in |- *; ring ].
unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with zarith.
unfold FtoR in |- *; replace (Fexp (Fminus radix y x)) with (Fexp x);
 auto with real.
unfold Fminus in |- *; simpl in |- *; auto with zarith.
rewrite Zmin_le2; auto with zarith.
apply Zle_trans with 0%Z; auto with zarith.
rewrite <- (Zopp_involutive (Fnum (Fminus radix y x))).
replace 0%Z with (- (0))%Z; auto with zarith; apply Zle_Zopp.
replace (- Fnum (Fminus radix y x))%Z with (Fnum (Fopp (Fminus radix y x)));
 [ idtac | unfold Fopp in |- *; simpl in |- × ].
apply (LeR0Fnum radix); auto.
rewrite Fopp_correct.
replace 0%R with (-0)%R; auto with real; apply Ropp_le_ge_contravar.
ring.
unfold Fminus in |- *; simpl in |- ×.
rewrite Zmin_le2; auto with zarith; unfold FboundedI in H'; intuition.
Qed.

Theorem SterbenzIAux2 :
  (x y : float) (n : nat),
 Zabs_nat (vNumInf b - vNumSup b) n
 FboundedI b x
 FcanonicI radix b y
 FboundedI b y
 (y x)%R
 (x 2%nat × y - n × powerRZ radix (Zmin (Fexp y) (Fexp x)))%R
 FboundedI b (Fminus radix y x).
intros x y n H H' Hcan H'0 H'1 H'2.
cut (Fminus radix y x 0)%R; [ intros Rle1 | idtac ].
2: rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- ×.
2: apply Rplus_le_reg_l with (r := FtoRradix x); auto.
2: replace (x + (y - x))%R with (FtoRradix y); [ idtac | ring ].
2: replace (x + 0)%R with (FtoRradix x); [ auto | simpl in |- *; ring ].
cut (- vNumInf b - vNumSup b + n)%Z; [ intros Zle1 | idtac ].
2: replace (- vNumSup b + n)%Z with (- (vNumSup b + - n))%Z;
    [ apply Zle_Zopp | ring ].
2: apply le_IZR; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
2: apply Rplus_le_reg_l with (n + - vNumInf b)%R.
2: apply Rle_trans with (vNumSup b - vNumInf b)%R;
    [ right; repeat rewrite <- INR_IZR_INZ; ring | idtac ].
2: apply Rle_trans with (INR n);
    [ idtac | right; rewrite <- INR_IZR_INZ; ring ].
2: rewrite <- (Rabs_right (vNumSup b)); auto with real arith.
2: rewrite <- (Rabs_right (vNumInf b)); auto with real arith.
2: apply Rle_trans with (Rabs (vNumSup b - vNumInf b));
    [ apply Rabs_triang_inv | idtac ].
2: rewrite <- Rabs_Ropp.
2: replace (- (vNumSup b - vNumInf b))%R with (vNumInf b - vNumSup b)%R;
    [ idtac | ring ].
2: repeat rewrite INR_IZR_INZ; rewrite Z_R_minus.
2: rewrite Faux.Rabsolu_Zabs; rewrite Zabs_absolu;
    auto with arith zarith real.
case (Zle_or_lt (Fexp y) (Fexp x)); intros Zle3.
apply SterbenzIAux2A with n; auto.
rewrite <- (Zmin_le1 (Fexp y) (Fexp x)); auto with zarith.
case (Rle_or_lt 0 y); intros Rle2.
absurd (Fexp x < Fexp y)%Z; auto.
apply Zle_not_lt.
apply LexicoPosCanI with radix b; auto.
apply SterbenzIAux2B with n; auto with zarith real float arith.
rewrite <- (Zmin_le2 (Fexp y) (Fexp x)); auto with zarith.
Qed.

Theorem SterbenzI :
  (x y : float) (n : nat),
 Zabs_nat (vNumInf b - vNumSup b) n
 FboundedI b xFcanonicI radix b xFboundedI b y
 (/ 2%nat × y + / 2%nat × (n × powerRZ radix (Zmin (Fexp x) (Fexp y))) x)%R
 (x 2%nat × y)%R
    FboundedI b (Fminus radix x y).
intros x y n Hn H H' H'0 H'1 H'2.
case (Rle_or_lt x y); intros Le2; auto.
apply SterbenzIAux2 with n; auto with real.
apply Rplus_le_reg_l with (n × powerRZ radix (Zmin (Fexp x) (Fexp y)))%R.
rewrite Rplus_comm.
apply Rle_trans with (2%nat × x)%R; [ idtac | right; ring ].
apply Rmult_le_reg_l with (r := (/ 2%nat)%R);
 [ apply Rinv_0_lt_compat; auto with real | idtac ].
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real;
 ring_simplify (1 × FtoRradix x)%R.
apply Rle_trans with (2 := H'1); right; ring.
apply SterbenzIAux1; auto with real.
Qed.

End FpropI.

Section SterbenzApproxIAux.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables (b1 : FboundI) (b2 : FboundI).

Theorem SterbenzApproxI_aux1 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumSup b1)) = (rho × Zsucc (vNumSup b2))%R
 (- dExpI b2 - dExpI b1)%Z
 FboundedI b1 x
 FboundedI b1 y
 (0 y)%R
 (y x)%R
 (x (1 + / rho) × y)%R
 FboundedI b2 (Fminus radix x (FnormalizeI radix b1 y)).
intros rho x y H1 H2 H'' H3 H4 H5 H6 H7.
cut (0 Fminus radix x (FnormalizeI radix b1 y))%R; [ intros Rle1 | idtac ].
2: rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- ×.
2: unfold FtoRradix in |- *; rewrite FnormalizeICorrect; auto.
2: apply Rplus_le_reg_l with (r := FtoR radix y); auto.
2: fold FtoRradix in |- *; ring_simplify; auto with real.
cut
 (Fexp (Fminus radix x (FnormalizeI radix b1 y)) =
  Fexp (FnormalizeI radix b1 y)); [ intros He | idtac ].
2: unfold Fminus in |- *; simpl in |- *; apply Zmin_le2.
2: apply LexicoPosCanI with radix b1; auto with zarith;
    [ apply FnormalizeIFcanonicI; auto | idtac | idtac ];
    rewrite FnormalizeICorrect; auto.
split; [ split | idtac ].
apply Zle_trans with 0%Z; auto with zarith; apply LeR0Fnum with radix; auto.
apply Zgt_succ_le; apply Zlt_gt; apply Zlt_Rlt.
apply
 Rle_lt_trans
  with ((x - y) × powerRZ radix (- Fexp (FnormalizeI radix b1 y)))%R.
right;
 apply
  trans_eq
   with
     (Fminus radix x (FnormalizeI radix b1 y) ×
      powerRZ radix (- Fexp (Fminus radix x (FnormalizeI radix b1 y))))%R.
unfold FtoRradix, FtoR in |- *; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify
    (Fexp (Fminus radix x (FnormalizeI radix b1 y)) +
     - Fexp (Fminus radix x (FnormalizeI radix b1 y)))%Z;
 simpl in |- *; ring.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite <- FnormalizeICorrect with radix b1 y; auto.
rewrite He; ring.
apply
 Rle_lt_trans
  with
    (/ rho × FtoRradix y × powerRZ radix (- Fexp (FnormalizeI radix b1 y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with (FtoRradix y); auto.
ring_simplify (FtoRradix y + (FtoRradix x - FtoRradix y))%R.
apply Rle_trans with (1 := H7); right; ring.
apply Rle_lt_trans with (/ rho × Fnum (FnormalizeI radix b1 y))%R.
unfold FtoRradix in |- *; rewrite <- FnormalizeICorrect with radix b1 y; auto.
right; unfold FtoR in |- ×.
apply
 trans_eq
  with
    (/ rho ×
     (powerRZ radix (- Fexp (FnormalizeI radix b1 y)) ×
      powerRZ radix (Fexp (FnormalizeI radix b1 y))) ×
     Fnum (FnormalizeI radix b1 y))%R.
ring.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify (- Fexp (FnormalizeI radix b1 y) + Fexp (FnormalizeI radix b1 y))%Z;
 simpl in |- *; ring.
apply Rlt_le_trans with (/ rho × Zsucc (vNumSup b1))%R.
apply Rmult_lt_compat_l; auto with real.
cut (FboundedI b1 (FnormalizeI radix b1 y));
 [ intros H8 | apply FnormalizeIBounded; auto ].
apply Rlt_IZR.
elim H8; intros H' H'1; elim H'; auto with zarith real.
right; rewrite H2; rewrite <- Rmult_assoc; rewrite Rinv_l;
 [ ring | auto with zarith real ].
apply Zle_trans with (- dExpI b1)%Z; auto with zarith; rewrite He.
cut (FboundedI b1 (FnormalizeI radix b1 y));
 [ intros H8 | apply FnormalizeIBounded; auto ].
elim H8; auto with zarith real.
Qed.

Theorem SterbenzApproxI_1 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumSup b1)) = (rho × Zsucc (vNumSup b2))%R
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
  FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 FboundedI b1 x
 FboundedI b1 y
 (/ (1 + / rho) × y x)%R
 (x (1 + / rho) × y)%R
  u : float, u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hv1 Hv2 Hv4 F1x F1y H1 H2.
cut (0 < 1 + / rho)%R; [ intros H' | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
    [ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
case (Rle_or_lt y x); intros H3.
case (Rcase_abs (FtoRradix y)); intros H4.
absurd (0 / rho × FtoRradix y)%R.
apply Rlt_not_le; replace 0%R with (/ rho × 0)%R; [ idtac | ring ].
apply Rmult_lt_compat_l; auto with real; apply Rinv_0_lt_compat;
 apply Rlt_le_trans with 1%R; auto with real.
apply Rplus_le_reg_l with (FtoRradix y); ring_simplify (FtoRradix y + 0)%R.
apply Rle_trans with (1 := H3); apply Rle_trans with (1 := H2); right; ring.
(Fminus radix x (FnormalizeI radix b1 y)); split.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite FnormalizeICorrect; auto with zarith.
apply SterbenzApproxI_aux1 with rho; auto with real float.
case (Rcase_abs (FtoRradix y)); intros H4.
absurd (0 / rho × FtoRradix y)%R.
apply Rlt_not_le; replace 0%R with (/ rho × 0)%R; [ idtac | ring ].
apply Rmult_lt_compat_l; auto with real.
apply Rplus_le_reg_l with (FtoRradix y); ring_simplify (FtoRradix y + 0)%R.
apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
apply Rle_trans with (1 := H1); apply Rle_trans with (FtoRradix y);
 auto with real.
right; apply trans_eq with (FtoRradix y × ((1 + / rho) × / (1 + / rho)))%R;
 [ idtac | ring; ring ].
rewrite Rinv_r; auto with real.
replace (FtoRradix x - FtoRradix y)%R with
 (- Fminus radix y (FnormalizeI radix b1 x))%R.
2: unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
2: rewrite FnormalizeICorrect; auto with zarith; ring.
apply Hv4.
apply SterbenzApproxI_aux1 with rho; auto with real float.
apply Rle_trans with (2 := H1); apply Rmult_le_pos; auto with real.
apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
apply Rle_trans with (1 := H1).
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
Qed.

Theorem SterbenzApproxI_aux2 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumSup b1)) = (rho × Zsucc (vNumInf b2))%R
 (- dExpI b2 - dExpI b1)%Z
 FboundedI b1 x
 FboundedI b1 y
 (0 y)%R
 (y x)%R
 (x (1 + / rho) × y)%R
 FboundedI b2 (Fminus radix (FnormalizeI radix b1 y) x).
intros rho x y H1 H2 H'' H3 H4 H5 H6 H7.
cut (Fminus radix (FnormalizeI radix b1 y) x 0)%R; [ intros Rle1 | idtac ].
2: rewrite (Fminus_correct radix); auto with zarith; fold FtoRradix in |- ×.
2: unfold FtoRradix in |- *; rewrite FnormalizeICorrect; auto.
2: apply Rplus_le_reg_l with (r := FtoR radix x); auto.
2: fold FtoRradix in |- *; ring_simplify; auto with real.
cut
 (Fexp (Fminus radix (FnormalizeI radix b1 y) x) =
  Fexp (FnormalizeI radix b1 y)); [ intros He | idtac ].
2: unfold Fminus in |- *; simpl in |- *; apply Zmin_le1.
2: apply LexicoPosCanI with radix b1; auto with zarith float real.
2: apply FnormalizeIFcanonicI; auto.
2: rewrite FnormalizeICorrect; auto.
2: rewrite FnormalizeICorrect; auto.
split; [ split | idtac ].
2: apply Zle_trans with 0%Z; auto with zarith; apply R0LeFnum with radix;
    auto.
2: apply Zle_trans with (- dExpI b1)%Z; auto with zarith; rewrite He.
2: cut (FboundedI b1 (FnormalizeI radix b1 y));
    [ intros H8 | apply FnormalizeIBounded; auto ].
2: elim H8; auto with zarith real.
apply Zle_Zopp_Inv; rewrite Zopp_involutive.
apply Zgt_succ_le; apply Zlt_gt; apply Zlt_Rlt.
apply
 Rle_lt_trans
  with ((x - y) × powerRZ radix (- Fexp (FnormalizeI radix b1 y)))%R.
right;
 apply
  trans_eq
   with
     (Fminus radix x (FnormalizeI radix b1 y) ×
      powerRZ radix (- Fexp (Fminus radix x (FnormalizeI radix b1 y))))%R.
unfold FtoRradix, FtoR in |- *; rewrite Rmult_assoc.
rewrite <- powerRZ_add; auto with zarith real.
apply
 trans_eq with (IZR (Fnum (Fopp (Fminus radix (FnormalizeI radix b1 y) x))));
 [ unfold Fopp in |- *; simpl in |- *; auto | rewrite Fopp_Fminus ].
ring_simplify
    (Fexp (Fminus radix x (FnormalizeI radix b1 y)) +
     - Fexp (Fminus radix x (FnormalizeI radix b1 y)))%Z;
 simpl in |- *; ring.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite <- FnormalizeICorrect with radix b1 y; auto.
replace (Fexp (Fminus radix x (FnormalizeI radix b1 y))) with
 (Fexp (Fminus radix (FnormalizeI radix b1 y) x)).
rewrite He; ring.
unfold Fminus in |- *; simpl in |- *; auto with zarith; apply Zmin_sym.
apply
 Rle_lt_trans
  with
    (/ rho × FtoRradix y × powerRZ radix (- Fexp (FnormalizeI radix b1 y)))%R.
apply Rmult_le_compat_r; auto with real zarith.
apply Rplus_le_reg_l with (FtoRradix y); auto.
ring_simplify (FtoRradix y + (FtoRradix x - FtoRradix y))%R.
apply Rle_trans with (1 := H7); right; ring.
apply Rle_lt_trans with (/ rho × Fnum (FnormalizeI radix b1 y))%R.
unfold FtoRradix in |- *; rewrite <- FnormalizeICorrect with radix b1 y; auto.
right; unfold FtoR in |- ×.
apply
 trans_eq
  with
    (/ rho ×
     (powerRZ radix (- Fexp (FnormalizeI radix b1 y)) ×
      powerRZ radix (Fexp (FnormalizeI radix b1 y))) ×
     Fnum (FnormalizeI radix b1 y))%R.
ring.
rewrite <- powerRZ_add; auto with zarith real.
ring_simplify (- Fexp (FnormalizeI radix b1 y) + Fexp (FnormalizeI radix b1 y))%Z;
 simpl in |- *; ring.
apply Rlt_le_trans with (/ rho × Zsucc (vNumSup b1))%R.
apply Rmult_lt_compat_l; auto with real.
cut (FboundedI b1 (FnormalizeI radix b1 y));
 [ intros H8 | apply FnormalizeIBounded; auto ].
apply Rlt_IZR.
elim H8; intros H' H'1; elim H'; auto with zarith real.
right; rewrite H2; rewrite <- Rmult_assoc; rewrite Rinv_l;
 [ ring | auto with zarith real ].
Qed.

Theorem SterbenzApproxI_2 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumSup b1)) = (rho × Zsucc (vNumInf b2))%R
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
  FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 FboundedI b1 x
 FboundedI b1 y
 (/ (1 + / rho) × y x)%R
 (x (1 + / rho) × y)%R
  u : float, u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hv1 Hv2 Hv4 F1x F1y H1 H2.
cut (0 < 1 + / rho)%R; [ intros H' | idtac ].
2: apply Rlt_trans with (1 + 0)%R;
    [ ring_simplify (1 + 0)%R | apply Rplus_lt_compat_l ]; auto with real.
case (Rle_or_lt y x); intros H3.
case (Rcase_abs (FtoRradix y)); intros H4.
absurd (0 / rho × FtoRradix y)%R.
apply Rlt_not_le; replace 0%R with (/ rho × 0)%R; [ idtac | ring ].
apply Rmult_lt_compat_l; auto with real; apply Rinv_0_lt_compat;
 apply Rlt_le_trans with 1%R; auto with real.
apply Rplus_le_reg_l with (FtoRradix y); ring_simplify (FtoRradix y + 0)%R.
apply Rle_trans with (1 := H3); apply Rle_trans with (1 := H2); right; ring.
replace (FtoRradix x - FtoRradix y)%R with
 (- Fminus radix (FnormalizeI radix b1 y) x)%R.
2: unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
2: rewrite FnormalizeICorrect; auto with zarith; ring.
apply Hv4.
apply SterbenzApproxI_aux2 with rho; auto with real float.
case (Rcase_abs (FtoRradix y)); intros H4.
absurd (0 / rho × FtoRradix y)%R.
apply Rlt_not_le; replace 0%R with (/ rho × 0)%R; [ idtac | ring ].
apply Rmult_lt_compat_l; auto with real.
apply Rplus_le_reg_l with (FtoRradix y); ring_simplify (FtoRradix y + 0)%R.
apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
apply Rle_trans with (1 := H1); apply Rle_trans with (FtoRradix y);
 auto with real.
right; apply trans_eq with (FtoRradix y × ((1 + / rho) × / (1 + / rho)))%R;
 [ idtac | ring; ring ].
rewrite Rinv_r; auto with real.
(Fminus radix (FnormalizeI radix b1 x) y); split.
unfold FtoRradix in |- *; rewrite Fminus_correct; auto with zarith.
rewrite FnormalizeICorrect; auto with zarith.
apply SterbenzApproxI_aux2 with rho; auto with real float.
apply Rle_trans with (2 := H1); apply Rmult_le_pos; auto with real.
apply Rmult_le_reg_l with (/ (1 + / rho))%R; auto with real.
apply Rle_trans with (1 := H1).
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
Qed.

End SterbenzApproxIAux.

Section SterbenzApproxI.
Variable radix : Z.
Hypothesis radixMoreThanOne : (1 < radix)%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
Variables (b1 : FboundI) (b2 : FboundI).

Theorem SterbenzApproxI_3 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumInf b1)) = (rho × Zsucc (vNumInf b2))%R
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
  FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 FboundedI b1 x
 FboundedI b1 y
 (x / (1 + / rho) × y)%R
 ((1 + / rho) × y x)%R
  u : float, u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hv1 Hv2 Hv3 Hx Hy Hxy1 Hxy2.
cut
 ( (b : FboundI) (z : float),
  FboundedI b z
  FboundedI (BoundI (vNumSup b) (vNumInf b) (dExpI b)) (Fopp z));
 [ intros V | intros b z Hz ].
2: elim Hz; intros Hz1 Hz2; elim Hz1; intros Hz3 Hz4; split; auto with zarith.
2: split; unfold Fopp in |- *; simpl in |- *; auto with zarith.
cut
 ( (b : FboundI) (z : float),
  FboundedI (BoundI (vNumSup b) (vNumInf b) (dExpI b)) z
  FboundedI b (Fopp z)); [ intros V' | intros b z Hz ].
2: elim Hz; simpl in |- *; intros Hz1 Hz2; elim Hz1; intros Hz3 Hz4; split;
    auto with zarith.
2: split; unfold Fopp in |- *; simpl in |- *; auto with zarith.
generalize SterbenzApproxI_1; intros H'.
elim
 H'
  with
    radix
    (BoundI (vNumSup b1) (vNumInf b1) (dExpI b1))
    (BoundI (vNumSup b2) (vNumInf b2) (dExpI b2))
    rho
    (Fopp x)
    (Fopp y); auto with zarith real float; clear H'.
2: intros u Hu; elim Hv3 with (Fopp u); auto.
2: intros v Hv; elim Hv; intros Hv1' Hv2'; clear Hv; (Fopp v); split;
    auto.
2: rewrite Fopp_correct; fold FtoRradix in |- *; rewrite Hv1';
    unfold FtoRradix in |- *; rewrite Fopp_correct;
    ring.
2: unfold FtoRradix in |- *; repeat rewrite Fopp_correct;
    fold FtoRradix in |- *; auto with real.
2: apply Ropp_le_cancel; rewrite Ropp_involutive;
    apply Rle_trans with (1 := Hxy1); right; ring.
2: repeat rewrite Fopp_correct; fold FtoRradix in |- *; auto with real.
2: apply Ropp_le_cancel; rewrite Ropp_involutive;
    apply Rle_trans with (2 := Hxy2); right; ring.
intros u Hu; elim Hu; intros Hu1 Hu2; clear Hu.
(Fopp u); split; auto.
unfold FtoRradix in |- *; rewrite Fopp_correct; rewrite Hu1;
 repeat rewrite Fopp_correct; ring.
Qed.

Theorem SterbenzApproxI_4 :
  (rho : R) (x y : float),
 (0 < rho)%R
 IZR (Zsucc (vNumInf b1)) = (rho × Zsucc (vNumSup b2))%R
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
  FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 FboundedI b1 x
 FboundedI b1 y
 (x / (1 + / rho) × y)%R
 ((1 + / rho) × y x)%R
  u : float, u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hv1 Hv2 Hv3 Hx Hy Hxy1 Hxy2.
cut
 ( (b : FboundI) (z : float),
  FboundedI b z
  FboundedI (BoundI (vNumSup b) (vNumInf b) (dExpI b)) (Fopp z));
 [ intros V | intros b z Hz ].
2: elim Hz; intros Hz1 Hz2; elim Hz1; intros Hz3 Hz4; split; auto with zarith.
2: split; unfold Fopp in |- *; simpl in |- *; auto with zarith.
cut
 ( (b : FboundI) (z : float),
  FboundedI (BoundI (vNumSup b) (vNumInf b) (dExpI b)) z
  FboundedI b (Fopp z)); [ intros V' | intros b z Hz ].
2: elim Hz; simpl in |- *; intros Hz1 Hz2; elim Hz1; intros Hz3 Hz4; split;
    auto with zarith.
2: split; unfold Fopp in |- *; simpl in |- *; auto with zarith.
generalize SterbenzApproxI_2; intros H'.
elim
 H'
  with
    radix
    (BoundI (vNumSup b1) (vNumInf b1) (dExpI b1))
    (BoundI (vNumSup b2) (vNumInf b2) (dExpI b2))
    rho
    (Fopp x)
    (Fopp y); auto with zarith real float; clear H'.
2: intros u Hu; elim Hv3 with (Fopp u); auto.
2: intros v Hv; elim Hv; intros Hv1' Hv2'; clear Hv; (Fopp v); split;
    auto.
2: rewrite Fopp_correct; fold FtoRradix in |- *; rewrite Hv1';
    unfold FtoRradix in |- *; rewrite Fopp_correct;
    ring.
2: unfold FtoRradix in |- *; repeat rewrite Fopp_correct;
    fold FtoRradix in |- *; auto with real.
2: apply Ropp_le_cancel; rewrite Ropp_involutive;
    apply Rle_trans with (1 := Hxy1); right; ring.
2: repeat rewrite Fopp_correct; fold FtoRradix in |- *; auto with real.
2: apply Ropp_le_cancel; rewrite Ropp_involutive;
    apply Rle_trans with (2 := Hxy2); right; ring.
intros u Hu; elim Hu; intros Hu1 Hu2; clear Hu.
(Fopp u); split; auto.
unfold FtoRradix in |- *; rewrite Fopp_correct; rewrite Hu1;
 repeat rewrite Fopp_correct; ring.
Qed.

Theorem SterbenzApproxI_pos :
  (rho : R) (x y : float),
 (0 < rho)%R
 rho =
 Rmin
   (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumInf b2))
      (Zsucc (vNumSup b1) / Zsucc (vNumSup b2)))
   (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumSup b2))
      (Zsucc (vNumSup b1) / Zsucc (vNumInf b2))) →
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
  FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 ( x : float,
  FboundedI b1 x y : float, y = (- x)%R :>R FboundedI b1 y) →
 FboundedI b1 x
 FboundedI b1 y
 (/ (1 + / rho) × y x)%R
 (x (1 + / rho) × y)%R
  u : float, u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hv1 Hv2 Hv3 Hv0 Hx Hy Hxy1 Hxy2.
cut ( u v : R, Rmin u v = u Rmin u v = v); [ intros V | idtac ].
2: intros u v; unfold Rmin in |- *; case (Rle_dec u v); auto.
case
 (V
    (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumInf b2))
       (Zsucc (vNumSup b1) / Zsucc (vNumSup b2)))
    (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumSup b2))
       (Zsucc (vNumSup b1) / Zsucc (vNumInf b2))));
 intros V1.
case
 (V (Zsucc (vNumInf b1) / Zsucc (vNumInf b2))%R
    (Zsucc (vNumSup b1) / Zsucc (vNumSup b2))%R); intros V2.
cut (rho = (Zsucc (vNumInf b1) / Zsucc (vNumInf b2))%R);
 [ intros Hv4; clear V2 V1 V Hv1 | rewrite Hv1; rewrite V1; auto with real ].
elim (Hv0 x); auto; intros Mx tmp; elim tmp; intros Mx1 Mx2; clear tmp.
elim (Hv0 y); auto; intros My tmp; elim tmp; intros My1 My2; clear tmp.
elim SterbenzApproxI_3 with rho Mx My; auto with real zarith.
2: rewrite Hv4; unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_l;
    auto with real zarith.
2: rewrite Mx1; rewrite My1; apply Ropp_le_cancel; rewrite Ropp_involutive;
    auto with real.
2: apply Rle_trans with (2 := Hxy1); right; ring.
2: rewrite Mx1; rewrite My1; apply Ropp_le_cancel; rewrite Ropp_involutive;
    auto with real.
2: apply Rle_trans with (1 := Hxy2); right; ring.
intros v tmp; elim tmp; intros Hv1' Hv2'; clear tmp.
replace (x - y)%R with (- (Mx - My))%R;
 [ rewrite <- Hv1'; auto with real | rewrite Mx1; rewrite My1; ring ].
cut (rho = (Zsucc (vNumSup b1) / Zsucc (vNumSup b2))%R);
 [ intros Hv4; clear V2 V1 V Hv1 | rewrite Hv1; rewrite V1; auto with real ].
unfold FtoRradix in |- *; apply SterbenzApproxI_1 with b1 rho;
 auto with real zarith.
rewrite Hv4; unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_l;
 auto with real arith zarith.
case
 (V (Zsucc (vNumInf b1) / Zsucc (vNumSup b2))%R
    (Zsucc (vNumSup b1) / Zsucc (vNumInf b2))%R); intros V2.
cut (rho = (Zsucc (vNumInf b1) / Zsucc (vNumSup b2))%R);
 [ intros Hv4; clear V2 V1 V Hv1 | rewrite Hv1; rewrite V1; auto with real ].
elim (Hv0 x); auto; intros Mx tmp; elim tmp; intros Mx1 Mx2; clear tmp.
elim (Hv0 y); auto; intros My tmp; elim tmp; intros My1 My2; clear tmp.
elim SterbenzApproxI_4 with rho Mx My; auto with real zarith.
2: rewrite Hv4; unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_l;
    auto with real zarith.
2: rewrite Mx1; rewrite My1; apply Ropp_le_cancel; rewrite Ropp_involutive;
    auto with real.
2: apply Rle_trans with (2 := Hxy1); right; ring.
2: rewrite Mx1; rewrite My1; apply Ropp_le_cancel; rewrite Ropp_involutive;
    auto with real.
2: apply Rle_trans with (1 := Hxy2); right; ring.
intros v tmp; elim tmp; intros Hv1' Hv2'; clear tmp.
replace (x - y)%R with (- (Mx - My))%R;
 [ rewrite <- Hv1'; auto with real | rewrite Mx1; rewrite My1; ring ].
cut (rho = (Zsucc (vNumSup b1) / Zsucc (vNumInf b2))%R);
 [ intros Hv4; clear V2 V1 V Hv1 | rewrite Hv1; rewrite V1; auto with real ].
unfold FtoRradix in |- *; apply SterbenzApproxI_2 with b1 rho;
 auto with real zarith.
rewrite Hv4; unfold Rdiv in |- *; rewrite Rmult_assoc; rewrite Rinv_l;
 auto with real zarith.
Qed.

Theorem SterbenzApproxI :
  (rho : R) (x y : float),
 (0 < rho)%R
 rho = Rmin
   (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumInf b2))
      (Zsucc (vNumSup b1) / Zsucc (vNumSup b2)))
   (Rmin (Zsucc (vNumInf b1) / Zsucc (vNumSup b2))
      (Zsucc (vNumSup b1) / Zsucc (vNumInf b2))) →
 (- dExpI b2 - dExpI b1)%Z
 ( x : float,
    FboundedI b2 x y : float, y = (- x)%R :>R FboundedI b2 y) →
 ( x : float,
    FboundedI b1 x y : float, y = (- x)%R :>R FboundedI b1 y) →
 FboundedI b1 xFboundedI b1 y
 (0 x × y)%R
 (/ (1 + / rho) × Rabs y Rabs x)%R
 (Rabs x (1 + / rho) × Rabs y)%R
    u : float,
     u = (x - y)%R :>R FboundedI b2 u.
intros rho x y Hrho Hrho2 Hv0 Hv2 Hv1 Hx Hy H1 H2 H3.
case (Rle_or_lt 0 y); intros H'0.
cut (0 x)%R; [ intros H'1 | idtac ].
apply SterbenzApproxI_pos with rho; auto; rewrite <- (Rabs_right y);
 auto with real; rewrite <- (Rabs_right x); auto with real.
case H'0; intros H'.
apply Rmult_le_reg_l with (FtoRradix y); auto with real.
ring_simplify; rewrite Rmult_comm; auto with real.
case (Req_dec 0 x); auto with real; intros H''.
absurd (0 < 0)%R; auto with real.
apply Rlt_le_trans with (Rabs (FtoRradix x)); auto with real.
apply Rabs_pos_lt; auto with real.
apply Rle_trans with (1 := H3); rewrite <- H'; rewrite Rabs_R0; right; ring.
cut (x 0)%R; [ intros H'1 | idtac ].
elim (Hv1 x); auto; intros Mx tmp; elim tmp; intros Mx1 Mx2; clear tmp.
elim (Hv1 y); auto; intros My tmp; elim tmp; intros My1 My2; clear tmp.
elim SterbenzApproxI_pos with rho Mx My; auto.
intros u tmp; elim tmp; intros Hu1 Hu2; clear tmp.
replace (FtoRradix x - FtoRradix y)%R with (- u)%R;
 [ idtac | rewrite Hu1; rewrite Mx1; rewrite My1; ring ].
apply Hv2; auto.
rewrite Mx1; rewrite My1; rewrite <- Faux.Rabsolu_left1; auto with real;
 rewrite <- Faux.Rabsolu_left1; auto with real.
rewrite Mx1; rewrite My1; rewrite <- Faux.Rabsolu_left1; auto with real;
 rewrite <- Faux.Rabsolu_left1; auto with real.
apply Rmult_le_reg_l with (- y)%R; auto with real.
ring_simplify;apply Rle_trans with (-(x×y))%R; auto with real.
right; ring.
Qed.

End SterbenzApproxI.