(** This proof file has been written by 
#<A href="http://perso.ens-lyon.fr/sylvie.boldo/">Sylvie Boldo</A>#(1), following a proof
presented by #<A HREF="http://www.cs.berkeley.edu/~wkahan/">Pr William Kahan</A># (2), 
and adapted to Coq proof checker with the help of 
#<A href="http://perso.ens-lyon.fr/guillaume.melquiond/">Guillaume Melquiond</A>#(1) 
and #<A href="http://perso.ens-lyon.fr/marc.daumas/">Marc Daumas</A>#(1). This work 
has been partially supported by the #<A HREF="http://www.cnrs.fr">CNRS</A># grant PICS 2533.

(1) #<A HREF="http://www.ens-lyon.fr/LIP/">LIP</A># Computer science laboratory
UMR 5668 CNRS - ENS de Lyon - INRIA
Lyon, France

(2) #<a href="http://www.berkeley.edu/">University of California at Berkeley</A>#
Berkeley, California
*)

Require Export AllFloat.

Section Discriminant1.
Variable bo : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.

Let FtoRradix := FtoR radix.
Coercion FtoRradix : float >-> R.
 
Theorem TwoMoreThanOne : (1 < radix)%Z.
unfold radix in |- *; red in |- *; simpl in |- *; auto.
Qed.
Hint Resolve TwoMoreThanOne.

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.


Variables a b b' c p q d:float.

Let delta := (Rabs (d-(b*b'-a*c)))%R.

Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).

(** There is no underflow *)
Hypothesis U1:(- dExp bo <= Fexp d - 1)%Z.
Hypothesis Nd:(Fnormal radix bo d).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Np:(Fnormal radix bo p).

Hypothesis Square:(0 <=b*b')%R.

Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).

Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R.
Hypothesis Roundd : (EvenClosest bo radix precision (p-q)%R d).




Theorem delta_inf: (delta <= (/2)*(Fulp bo radix precision d)+
   ((/2)*(Fulp bo radix precision p)+(/2)*(Fulp bo radix precision q)))%R.
unfold delta; rewrite <- Rabs_Ropp.
replace (-(d - (b * b' - a * c)))%R with (((p-q)-d)+((b*b'-p)+-(a*c-q)))%R;[idtac|ring].
apply Rle_trans with ((Rabs ((p-q)-d))+(Rabs (b * b' - p + - (a * c - q))))%R;
  [apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundd; auto.
right; simpl; field; auto with real.
apply Rle_trans with ((Rabs (b*b'-p))+(Rabs (-(a*c-q))))%R;
  [apply Rabs_triang|idtac].
apply Rplus_le_compat.
apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundp; auto.
right; simpl; field; auto with real.
rewrite Rabs_Ropp; apply Rmult_le_reg_l with (S (S O)); auto with arith real.
apply Rle_trans with (Fulp bo radix precision q).
unfold FtoRradix; apply ClosestUlp;auto with zarith.
elim Roundq; auto.
right; simpl; field; auto with real.
Qed.

Theorem P_positive: (Rle 0 p)%R.
unfold FtoRradix; apply RleRoundedR0 with (b:=bo) (precision:=precision) (P:=(Closest bo radix)) (r:=(b*b')%R); auto.
apply ClosestRoundedModeP with precision; auto.
elim Roundp; auto.
Qed.

Theorem Fulp_le_twice_l: forall x y:float, (0 <= x)%R -> 
   (Fnormal radix bo x) -> (Fbounded bo y) -> (2*x<=y)%R -> 
   (2*(Fulp bo radix precision x) <= (Fulp bo radix precision y))%R. 
intros.
assert (2*x=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum x) (Zsucc (Fexp x)))).
right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
simpl; ring.
elim H0; intros H4 H5; elim H4; intros.
left; split; auto.
split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H4 H5; elim H4; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; apply Rmult_le_pos; auto with real.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.

Theorem Fulp_le_twice_r: forall x y:float, (0 <= x)%R -> 
   (Fnormal radix bo y) -> (Fbounded bo x) -> (x<=2*y)%R -> 
   ((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R. 
intros.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H0; intros H6 H5; elim H6; intros.
2:split; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H0; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
fold FtoRradix; rewrite <- H3; auto with real.
Qed.



Theorem Half_Closest_Round: forall (x:float) (r:R), 
   (- dExp bo <= Zpred (Fexp x))%Z -> (Closest bo radix r x)
  -> (Closest bo radix (r/2)%R (Float (Fnum x) (Zpred (Fexp x)))).
intros x r L H.
assert (x/2=(Float (Fnum x) (Zpred (Fexp x))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; field.
elim H; intros H2 H3.
split; [split; simpl; auto with float zarith|idtac].
intros. 
fold FtoRradix; rewrite <- H0.
replace (x/2-r/2)%R with (/2*(x-r))%R;[idtac|unfold Rdiv; ring]. 
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
replace (f-r/2)%R with (/2*((Float (Fnum f) (Zsucc (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (/2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H3.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; field; auto with real.
Qed.

Theorem Twice_EvenClosest_Round: forall (x:float) (r:R), 
   (-(dExp bo) <= (Fexp x)-1)%Z -> (Fnormal radix bo x)
  -> (EvenClosest bo radix precision r x)
  -> (EvenClosest bo radix precision (2*r)%R (Float (Fnum x) (Zsucc (Fexp x)))).
intros x r U Nx H.
assert (x*2=(Float (Fnum x) (Zsucc (Fexp x))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; ring.
elim H; intros H2 H3; elim H2; intros H'1 H'2; split.
split; [split; simpl; auto with float zarith|idtac].
intros.
fold FtoRradix; rewrite <- H0.
replace (x*2-2*r)%R with (2*(x-r))%R;[idtac|unfold Rdiv; ring]. 
rewrite Rabs_mult; rewrite Rabs_right; auto with real.
2: apply Rle_ge; auto with real.
case (Zle_lt_or_eq (-(dExp bo))%Z (Fexp f)); auto with zarith float; intros L.
replace (f-2*r)%R with (2*((Float (Fnum f) (Zpred (Fexp f)))-r))%R.
rewrite Rabs_mult; rewrite Rabs_right with (2)%R.
2: apply Rle_ge; auto with real.
apply Rmult_le_compat_l; auto with real.
unfold FtoRradix; apply H'2.
split; simpl; auto with zarith float.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; field; auto with real.
replace (f-2*r)%R with (-((2*r)-f))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (2:=Rabs_triang_inv (2*r)%R f).
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge;auto with real.
pattern r at 2 in |-*; replace r with (x-(x-r))%R;[idtac|ring].
apply Rle_trans with (2*(Rabs (x)-Rabs (x-r))-Rabs f)%R;[idtac|unfold Rminus; apply Rplus_le_compat_r; apply Rmult_le_compat_l; auto with real].
2: generalize (Rabs_triang_inv x (x-r)%R); unfold Rminus; auto with real.
apply Rplus_le_reg_l with (Rabs f -2*(Rabs (x-r)))%R.
apply Rle_trans with (Rabs f);[right;ring|idtac].
apply Rle_trans with (2*(Rabs x)-4*Rabs (x-r))%R;[idtac|right;ring].
apply Rle_trans with (((powerRZ radix precision)-1)*(powerRZ radix ((Fexp x)-1)))%R.
unfold FtoRradix; rewrite <- Fabs_correct; auto;unfold Fabs, FtoR; simpl.
apply Rmult_le_compat; auto with real zarith.
apply Rle_trans with (Zpred (Zpower_nat radix precision));[rewrite <- pGivesBound|idtac].
apply Rle_IZR;apply Zle_Zpred; auto with float.
unfold Zpred; rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
rewrite <- L; apply Rle_powerRZ; auto with real zarith.
apply Rle_trans with (2*(powerRZ radix (Zpred precision))*(powerRZ radix (Fexp x))-2*(powerRZ radix (Fexp x)))%R.
apply Rle_trans with (((powerRZ radix (precision+1))-4)*(powerRZ radix (Fexp x-1)))%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
rewrite powerRZ_add; auto with real zarith; simpl.
apply Rplus_le_reg_l with (-(powerRZ 2 precision)+4)%R.
ring_simplify.
apply Rle_trans with (powerRZ 2 2)%R; auto with real zarith.
simpl; ring_simplify (2*(2*1))%R; auto with real zarith.
apply Rle_trans with (3+1)%R; auto with real; right; ring.
apply Rle_powerRZ; auto with arith zarith real.
replace (2*powerRZ radix (Fexp x))%R with (4*powerRZ radix (Fexp x -1))%R.
pattern 2%R at 3 in |-*; replace 2%R with (powerRZ radix 1%Z);[idtac|simpl; ring].
repeat rewrite <- powerRZ_add; auto with real zarith.
replace (1+Zpred precision+Fexp x)%Z with ((precision+1)+(Fexp x-1))%Z;[idtac|unfold Zpred; ring].
rewrite powerRZ_add with (n:=(precision+1)%Z);auto with real zarith; right;ring.
unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl; field.
unfold Rminus; apply Rplus_le_compat;[rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|apply Ropp_le_contravar].
unfold FtoRradix; rewrite <- Fabs_correct; auto; unfold FtoR, Fabs; simpl.
apply Rmult_le_compat_r; auto with real zarith.
apply Rmult_le_reg_l with radix; auto with real zarith.
pattern (IZR radix) at 1 in |-*; replace (IZR radix) with (powerRZ radix 1%Z);[idtac|simpl; ring].
rewrite <- powerRZ_add; auto with real zarith; elim Nx; intros.
replace (1+Zpred precision)%Z with (Z_of_nat precision)%Z;[idtac|unfold Zpred; ring].
apply Rle_trans with (IZR (Zpos (vNum bo)));[rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith|idtac].
apply Rle_trans with (IZR (Zabs (radix * Fnum x))); auto with real zarith.
rewrite Zabs_Zmult; rewrite Zabs_eq; auto with real zarith.
rewrite mult_IZR; auto with real.
replace 4%R with (2*2%nat)%R; [rewrite Rmult_assoc; apply Rmult_le_compat_l; auto with real|simpl;ring].
replace (x+-r)%R with (-(r-x))%R;[rewrite Rabs_Ropp|ring].
apply Rle_trans with (Fulp bo radix precision x).
unfold FtoRradix; apply ClosestUlp; auto.
rewrite CanonicFulp; auto with real zarith.
right; unfold FtoR; simpl; ring.
left; auto.
case H3; intros V.
left; generalize V; unfold FNeven; rewrite FcanonicFnormalizeEq; auto with zarith.
rewrite FcanonicFnormalizeEq; auto with zarith.
elim Nx; intros; left; split; auto with zarith.
elim H1; intros; split; simpl; auto with zarith.
left; auto.
right; intros.
apply trans_eq with (2*(FtoR radix (Float (Fnum q0) (Zpred (Fexp q0)))))%R.
unfold FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; field; auto with real.
apply trans_eq with (2*(FtoR radix x))%R;[idtac|unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith; simpl; ring].
apply Rmult_eq_compat_l; apply V.
replace r with ((2*r)/2)%R;[idtac|field; auto with real].
apply Half_Closest_Round; auto.
apply Zle_trans with (1:=U).
fold (Zpred (Fexp x)); cut (Fexp x <= Fexp q0)%Z; auto with zarith.
apply Zle_trans with (Fexp (Fnormalize radix bo precision q0)).
apply Fcanonic_Rle_Zle with radix bo precision; auto with zarith.
left; auto.
apply FnormalizeCanonic; auto with arith.
elim H1; auto.
generalize ClosestMonotone; unfold MonotoneP; intros.
repeat rewrite <- Fabs_correct; auto.
apply H4 with bo (Rabs r) (Rabs (2*r))%R.
rewrite Rabs_mult; rewrite (Rabs_right 2%R); try apply Rle_ge; auto with real.
apply Rle_lt_trans with (1*Rabs r)%R;[right;ring|apply Rmult_lt_compat_r; auto with real].
apply Rabs_pos_lt;unfold not;intros.
absurd (is_Fzero x).
apply FnormalNotZero with radix bo ; auto.
apply is_Fzero_rep2 with radix; auto.
cut (0 <= FtoR radix x)%R; intros.
cut (FtoR radix x <= 0)%R; intros; auto with real.
apply RleRoundedLessR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply RleRoundedR0 with bo precision (Closest bo radix) r; auto with real.
apply ClosestRoundedModeP with precision; auto.
apply ClosestFabs with precision; auto.
apply ClosestFabs with precision; auto.
generalize ClosestCompatible; unfold CompatibleP; intros T.
apply T with (2*r)%R q0; auto with real float zarith.
apply sym_eq;apply FnormalizeCorrect; auto.
apply FnormalizeBounded; auto with zarith.
elim H1; auto.
apply FcanonicLeastExp with radix bo precision; auto with zarith float.
apply sym_eq; apply FnormalizeCorrect; auto.
elim H1; auto.
apply FnormalizeCanonic; auto with zarith;elim H1; auto.
Qed.


Theorem EvenClosestMonotone2: forall (p q : R) (p' q' : float),
  (p <= q)%R -> (EvenClosest bo radix precision p p') -> 
  (EvenClosest bo radix precision q q') -> (p' <= q')%R.
intros.
case H; intros H2.
generalize EvenClosestMonotone; unfold MonotoneP.
intros W; unfold FtoRradix.
apply W with bo precision p0 q0; auto.
generalize EvenClosestUniqueP; unfold UniqueP.
intros W; unfold FtoRradix.
right; apply W with bo precision p0; auto with real.
rewrite H2; auto.
Qed.


Theorem Fulp_le_twice_r_round: forall (x y:float) (r:R), (0 <= x)%R -> 
   (Fbounded bo x) -> (Fnormal radix bo y) -> (- dExp bo <= Fexp y - 1)%Z
     -> (x<=2*r)%R ->
   (EvenClosest bo radix precision r y) -> 
   ((Fulp bo radix precision x) <= 2*(Fulp bo radix precision y))%R.
intros x y r H H0 H1 U H2 H3.
assert (2*y=(Float (Fnum y) (Zsucc (Fexp y))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum y) (Zsucc (Fexp y)))).
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H1; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real.
elim H1; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
apply EvenClosestMonotone2 with x (2*r)%R; auto.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Twice_EvenClosest_Round; auto.
Qed.


Theorem discri1: (delta <= 2*(Fulp bo radix precision d))%R.
apply Rle_trans with (1:=delta_inf).
case (Rle_or_lt q p); intros H1.
case (Rle_or_lt 0%R q); intros H2.
cut (2*(Fulp bo radix precision q)<=(Fulp bo radix precision p))%R; try intros H3.
cut ((Fulp bo radix precision p)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
    (/ 2 * (2*Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
apply Fulp_le_twice_r_round with (p-q)%R; auto.
apply P_positive.
apply Rplus_le_reg_l with (2*q-p)%R.
ring_simplify.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Fulp_le_twice_l; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-3*q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_right.
right; ring.
apply Rle_ge; apply Rplus_le_reg_l with q; ring_simplify; auto with real.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
    (/ 2 * (Fulp bo radix precision d) + / 2 * Fulp bo radix precision d)))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
apply LeFulpPos; auto with real.
fold FtoRradix; apply P_positive.
fold FtoRradix; apply EvenClosestMonotone2 with p (p-q)%R; auto.
apply Rle_trans with (p-0)%R; unfold Rminus; auto with real; right;ring.
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
apply Rmult_le_compat; auto with real.
unfold Fulp; auto with real zarith.
rewrite FulpFabs; auto.
apply LeFulpPos; auto with real.
split; auto with zarith float.
rewrite Fabs_correct; auto with real.
fold FtoRradix; apply EvenClosestMonotone2 with (-q)%R (p-q)%R; auto.
generalize P_positive; intros; auto with real.
apply Rle_trans with (0-q)%R; unfold Rminus; auto with real; right;ring.
replace (-q)%R with (FtoRradix (Fabs q)).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; auto with zarith float.
unfold FtoRradix;rewrite Fabs_correct; auto with real; rewrite Rabs_left; auto with real.
apply Rle_trans with ((3*/2)*(Fulp bo radix precision d))%R.
right; field; auto with real.
apply Rmult_le_compat_r;auto with zarith real.
unfold Fulp; auto with zarith real.
apply Rmult_le_reg_l with 2%R;auto with real.
apply Rle_trans with 3%R; auto with real.
right; field; auto with real.
replace 3%R with (IZR 3); auto with real zarith.
replace 4%R with (IZR 4); auto with real zarith.
simpl; ring.
simpl; ring.
cut (2*(Fulp bo radix precision p)<=(Fulp bo radix precision q))%R; try intros H3.
cut ((Fulp bo radix precision q)<=2*(Fulp bo radix precision d))%R; try intros H4.
apply Rle_trans with ((/ 2 * Fulp bo radix precision d +
    (/ 2 * (Fulp bo radix precision d) + / 2 * (2*Fulp bo radix precision d))))%R.
apply Rplus_le_compat; auto with real.
apply Rplus_le_compat; auto with real.
apply Rmult_le_compat_l; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (1:=H3); auto with real.
right; field; auto with real.
assert (p-q <=0)%R.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
rewrite FulpFabs with bo radix precision d; auto.
apply Fulp_le_twice_r_round with (Rabs (p-q))%R; auto.
apply Rle_trans with p; auto with real; apply P_positive.
apply FnormalFabs; auto.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (p-q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
generalize EvenClosestSymmetric; unfold SymmetricP; intros.
rewrite Rabsolu_left1; auto with real.
replace (Fabs d) with (Fopp d).
apply H0; auto.
unfold Fabs, Fopp; replace (Zabs (Fnum d)) with (-(Fnum d))%Z; auto.
rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith.
cut (Fnum d <= 0)%Z; auto with zarith.
apply R0LeFnum with radix; auto.
apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (p-q)%R; auto with real zarith.
apply EvenClosestRoundedModeP; auto.
apply Fulp_le_twice_l; auto.
apply P_positive.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (-3*p+q)%R.
ring_simplify.
apply Rle_trans with (1:=Firstcase); rewrite Rabs_left1; auto.
right; ring.
apply Rplus_le_reg_l with q.
ring_simplify; auto with real.
Qed.

End Discriminant1.

Section Discriminant2.
Variable bo : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.

Variables a b b' c p q t dp dq s d:float.

Let delta := (Rabs (d-(b*b'-a*c)))%R.

Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).

(** There is no underflow *)
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (- dExp bo <= Fexp a + Fexp c - precision)%Z.
Hypothesis U3: (- dExp bo <= Fexp q - precision)%Z.
Hypothesis U4: (- dExp bo <= Fexp b + Fexp b' - precision)%Z.
Hypothesis U5: (- dExp bo <= Fexp p - precision)%Z.


Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Ns:(Fnormal radix bo s).
Hypothesis Nd:(Fnormal radix bo d).


Hypothesis Square:(0 <=b*b')%R.

Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).

Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.

Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq   : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq   : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).

Hypothesis p_differ_q:~(p=q)%R.

Theorem Q_positive:(0 < q)%R.
case (Rle_or_lt q 0%R); auto; intros.
absurd (3*(Rabs (p-q)) < (Rabs (p-q)))%R.
apply Rle_not_lt; apply Rle_trans with (1*(Rabs (p-q)))%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (IZR 1); auto with real.
apply Rle_trans with (IZR 3); auto with real zarith.
simpl; auto with real zarith.
apply Rlt_le_trans with (1:=Secondcase).
apply Rle_trans with (2:=Rabs_triang_inv p q).
right; rewrite Rabs_right.
rewrite Rabs_left1; auto with real; ring.
apply Rle_ge; apply P_positive with bo precision b b'; auto.
Qed.

Theorem Q_le_two_P:(q <= 2*p)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*q-q)%R; [right; ring|idtac].
pattern (FtoRradix q) at 1; rewrite <- (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
pattern (FtoRradix q) at 1; replace (FtoRradix q) with (-(p-q)+p)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (-(p-q))+(Rabs p))-q)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite Rabs_Ropp.
rewrite (Rabs_right p).
2:apply Rle_ge; apply P_positive with bo precision b b'; auto.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*p - q))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*p-q))%R; auto with real.
right;ring.
Qed.



Theorem P_le_two_Q:(p <= 2*q)%R.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real; simpl.
apply Rle_trans with (3*p-p)%R; [right; ring|idtac].
pattern (FtoRradix p) at 1; rewrite <- (Rabs_right p).
2: apply Rle_ge; apply P_positive with bo precision b b'; auto with real.
pattern (FtoRradix p) at 1; replace (FtoRradix p) with ((p-q)+q)%R;[idtac|ring].
apply Rle_trans with (3*(Rabs (p-q)+(Rabs q))-p)%R.
unfold Rminus; apply Rplus_le_compat_r.
apply Rmult_le_compat_l; auto with real.
apply Rle_trans with 2%R; auto with real.
apply Rabs_triang.
rewrite (Rabs_right q).
2: apply Rle_ge; generalize Q_positive; auto with real.
apply Rle_trans with (3 * (Rabs (p - q)) + (3*q - p))%R;[right;ring|idtac].
apply Rle_trans with (p+q+(3*q-p))%R; auto with real.
right;ring.
Qed.



Theorem t_exact: (FtoRradix t=p-q)%R.
unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith.
apply sym_eq; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto.
apply EvenClosestRoundedModeP; auto.
2: rewrite Fminus_correct; auto with zarith.
apply Sterbenz; auto.
fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real. 
apply Rle_trans with (FtoRradix q);[simpl; right; field; auto with real|idtac].
apply Q_le_two_P.
fold FtoRradix; simpl; apply P_le_two_Q.
Qed.

Theorem dp_dq_le:(Rabs (dp-dq) <= (3/2)*(Rmin
    (Fulp bo radix precision p) (Fulp bo radix precision q)))%R. 
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)).
rewrite Rabs_Ropp;apply Rmult_le_reg_l with (S (S O))%R; auto with real.
apply Rle_trans with (S 1 * Rabs dp + S 1*Rabs dq)%R;[right;ring|idtac].
apply Rle_trans with ((Fulp bo radix precision p)+(Fulp bo radix precision q))%R.
apply Rplus_le_compat.
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite <- Rmult_assoc.
apply Rle_trans with (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R;[idtac|apply Rmult_le_compat_r].
2: unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1; unfold Fulp; auto with real zarith.
2: right; simpl; unfold Rdiv; field; auto with real.
unfold Rmin; case (Rle_dec (Fulp bo radix precision p) (Fulp bo radix precision q)); intros H1.
apply Rle_trans with (Fulp bo radix precision p+2*Fulp bo radix precision p)%R;[apply Rplus_le_compat_l|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
generalize Q_positive; auto with real.
apply Q_le_two_P.
apply Rle_trans with (2*Fulp bo radix precision q+Fulp bo radix precision q)%R;[apply Rplus_le_compat_r|right;ring].
apply Fulp_le_twice_r; auto with real; fold radix FtoRradix.
apply P_positive with bo precision b b'; auto with real.
apply P_le_two_Q.
Qed.


Theorem EvenClosestFabs :
 forall (f : float) (r : R), (Fcanonic radix bo f)
    -> EvenClosest bo radix precision r f -> 
    EvenClosest bo radix precision (Rabs r) (Fabs f).
intros.
case (Rle_or_lt 0%R r); intros.
rewrite Rabs_right; auto with real.
unfold Fabs; rewrite Zabs_eq; auto with zarith.
apply LeR0Fnum with (radix := radix); auto with zarith.
apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) r; auto with float zarith.
rewrite Rabs_left; auto with real.
replace (Fabs f) with (Fopp f).
generalize EvenClosestSymmetric; unfold SymmetricP; auto.
unfold Fabs, Fopp; rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto.
assert (Fnum f <= 0)%Z; auto with zarith.
apply R0LeFnum with (radix:=radix); auto with zarith.
apply RleRoundedLessR0 with  bo precision (EvenClosest bo radix precision) r; auto with float zarith real.
Qed.



Theorem discri2: (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q))
  <= (Rabs (p-q)))%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; unfold delta.
apply Rle_trans with (1 * Fulp bo radix precision d)%R;[ring_simplify (1 * Fulp bo radix precision d)%R | unfold Fulp; auto with real zarith].
replace  (d - (b * b' - a * c))%R with ((d-(t+s))+(t+s-b*b'+a*c))%R;[idtac|ring].
apply Rle_trans with (1:=Rabs_triang (d-(t+s))%R (t + s - b * b' + a * c)%R).
apply Rmult_le_reg_l with 2%R; auto with real.
rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision d+Fulp bo radix precision d)%R;[idtac|right;ring].
apply Rplus_le_compat.
rewrite <- Rabs_Ropp; replace (- (d - (t + s)))%R with ((t+s)-d)%R;[idtac|ring].
replace 2%R with (INR 2); auto with real.
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite t_exact.
replace (p - q + s - b * b' + a * c)%R with (-((dp-dq) - s))%R;[idtac|rewrite dpEq; rewrite dqEq; ring].
rewrite Rabs_Ropp; apply Rle_trans with (Fulp bo radix precision s).
unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto.
rewrite FulpFabs; auto; rewrite FulpFabs with (f:=d); auto.
apply LeFulpPos; auto with real zarith float.
rewrite Fabs_correct; auto with real.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq)) (Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply EvenClosestFabs; auto; left; auto.
cut (Rabs (dp - dq) <= (Rabs (p-q))/2)%R.
intros H2; cut ((Rabs s) <= (Rabs t)/2)%R.
intros H3; apply Rle_trans with (1:=H2).
rewrite <- t_exact; apply Rle_trans with ((Rabs t)-(Rabs t)/2)%R.
right; unfold Rdiv; field; auto with real.
apply Rle_trans with ((Rabs t)-(Rabs s))%R; auto with real.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
replace (t+s)%R with (t-(-s))%R; [idtac|ring].
apply Rle_trans with ((Rabs t)-(Rabs (-s)))%R;[idtac|apply Rabs_triang_inv].
rewrite Rabs_Ropp; auto with real.
assert (t/2=(Float (Fnum t) (Zpred (Fexp t))))%R.
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith;  simpl ; field.
unfold Rdiv; rewrite <- (Rabs_right (/2)%R); auto with real.
2: apply Rle_ge; apply Rlt_le; auto with real.
rewrite <- Rabs_mult; fold (Rdiv t 2%R).
rewrite H; unfold FtoRradix; rewrite <- Fabs_correct; auto.
rewrite <- Fabs_correct; auto.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (Rabs (p-q)/2)%R; auto.
apply EvenClosestFabs; auto; left; auto.
replace (Rabs (p - q) / 2)%R with (FtoRradix (Fabs (Float (Fnum t) (Zpred (Fexp t))))).
unfold FtoRradix; apply RoundedModeProjectorIdem with (b:=bo) (P:=(EvenClosest bo radix precision)); auto.
apply EvenClosestRoundedModeP; auto.
split; simpl; auto with zarith float.
rewrite Zabs_eq; auto with zarith float.
unfold FtoRradix; rewrite Fabs_correct; auto; fold FtoRradix; rewrite <- H.
rewrite t_exact; unfold Rdiv; rewrite Rabs_mult; auto with real.
rewrite (Rabs_right (/2)%R); auto with real.
apply Rle_ge; apply Rlt_le; auto with real.
apply Rle_trans with (1:=dp_dq_le).
apply Rmult_le_reg_l with 2%R; auto with real; unfold Rdiv.
rewrite <- Rmult_assoc.
replace (2*(3*/2))%R with 3%R;[idtac|field; auto with real].
apply Rle_trans with (1:=H1).
right; field; auto with real.
Qed.

Theorem discri3: (exists f:float, (Fbounded bo f) /\ (FtoRradix f)=(dp-dq)%R) 
    -> (delta <= 2*(Fulp bo radix precision d))%R.
intros T; elim T; intros f T1; elim T1; intros H1 H2; clear T T1.
unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d))%R.
apply Rmult_le_reg_l with (INR 2); auto with arith real.
apply Rle_trans with (Fulp bo radix precision d).
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
simpl; apply Rle_trans with (1*(1*(Fulp bo radix precision d)))%R; unfold Fulp; auto with real zarith.
right; ring.
apply Rmult_le_compat; auto with real zarith.
ring_simplify   (1 * powerRZ radix (Fexp (Fnormalize radix bo precision d)))%R; auto with real zarith.
replace (FtoRradix s) with (dp-dq)%R.
rewrite dpEq; rewrite dqEq; rewrite t_exact; ring.
rewrite <- H2.
unfold FtoRradix; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto with real.
apply EvenClosestRoundedModeP; auto.
fold FtoRradix; rewrite H2; auto.
Qed.


Theorem errorBoundedMultClosest_Can:
       forall f1 f2 g : float,
       Fbounded bo f1 ->
       Fbounded bo f2 ->
       Closest bo radix (f1* f2) g ->
       (- dExp bo <= Fexp f1 + Fexp f2 - precision)%Z ->
       (- dExp bo <= Fexp g - precision)%Z ->
       Fcanonic radix bo g ->
         (exists s : float,
            Fbounded bo s /\
           (FtoRradix s = f1*f2 - g)%R /\
            Fexp s = (Fexp g - precision)%Z /\
            (Rabs (Fnum s) <= powerRZ radix (Zpred precision))%R).
intros.
generalize errorBoundedMultClosest; intros T.
elim T with (b:=bo) (radix:=radix) (precision:=precision) (p:=f1) (q:=f2) (pq:=g); auto with zarith real; clear T; fold FtoRradix.
intros g' T1; elim T1; intros dg T2; elim T2; intros H5 T3; elim T3; intros H6 T4; elim T4; intros H7 T5; elim T5; intros H8 T6; elim T6; intros H9 H10; clear T1 T2 T3 T4 T5 T6.
exists dg; split; auto; split.
rewrite <- H8; auto with real.
split; [replace g with g'; auto with zarith|idtac].
apply FcanonicUnique with radix bo precision; auto with arith.
apply Rmult_le_reg_l with (powerRZ radix (Fexp dg)); auto with zarith real.
apply Rle_trans with (Rabs dg);[right; unfold FtoRradix, FtoR|idtac].
rewrite Rabs_mult;rewrite (Rabs_right (powerRZ radix (Fexp dg)));auto with real.
apply Rle_ge; auto with real zarith.
rewrite H9; rewrite <- powerRZ_add; auto with real zarith.
apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision g').
unfold FtoRradix; apply ClosestUlp; auto.
replace g' with g; auto.
apply FcanonicUnique with radix bo precision; auto with arith.
rewrite CanonicFulp; auto.
right; apply trans_eq with (powerRZ radix (Fexp g'));[unfold FtoR; simpl; ring|idtac].
apply trans_eq with ((powerRZ radix 1%Z)*(powerRZ radix (Fexp dg+Zpred precision)))%R;[rewrite <- powerRZ_add; auto with zarith real|simpl; ring].
rewrite H10; unfold Zpred; auto with zarith real.
ring_simplify (1 + (Fexp g' - precision + (precision + -1)))%Z; auto with real.
rewrite FcanonicFnormalizeEq; auto with zarith.
Qed.


Theorem discri4: (Fexp p)=(Fexp q) -> (delta <= 2*(Fulp bo radix precision d))%R.
intros H1; apply discri3.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=b) (f2:=b') (g:=p); auto with zarith real; clear T.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
generalize errorBoundedMultClosest_Can; intros T.
elim T with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear T.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
assert ((Rabs (Fnum dp'-Fnum dq') < (powerRZ radix precision))%R \/ 
 (((Rabs dp')= (powerRZ radix (Zpred (Fexp p))))%R /\  ((Rabs dq')= (powerRZ radix (Zpred (Fexp p))))%R)).
case H5; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp') (-(Fnum dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp'))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4'; rewrite H4; unfold Zpred.
ring_simplify (precision + -1 + (Fexp p - precision))%Z; 
  ring_simplify (precision + -1 + (Fexp q - precision))%Z; 
    ring_simplify (Fexp p+-1)%Z; rewrite <- H1; auto with zarith real.
case H; clear H; intros H.
exists (Float ((Fnum dp')-(Fnum dq'))%Z (Fexp dq')).
split; [split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; replace (Fexp dp') with (Fexp dq');[ring|idtac].
rewrite H4'; rewrite <- H1; auto with zarith.
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
elim H; unfold Rabs; case (Rcase_abs dp'); case (Rcase_abs dq'); intros.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl|idtac];ring.
exists (Float (-2)%Z (Zpred (Fexp p))); split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
apply trans_eq with (-(-dp')+-dq')%R;[rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl|idtac];ring.
exists (Float 2%Z (Zpred (Fexp p))); split;[split;simpl;auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.
unfold Rminus;rewrite H0; rewrite H6; unfold FtoRradix, FtoR;simpl; ring.
exists (Float 0%Z 0%Z); split;[split; auto with zarith|idtac].
simpl; case (dExp bo); auto with zarith.
rewrite H0; rewrite H6; unfold FtoRradix, FtoR; simpl;ring.
Qed.

End Discriminant2.

Section Discriminant3.
Variable bo : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.

Variables a b b' c p q t dp dq s d:float.

Let delta := (Rabs (d-(b*b'-a*c)))%R.

Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fb': (Fbounded bo b').
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).


(** There is no underflow *)
Hypothesis U1: (- dExp bo <= Fexp p - precision)%Z.
Hypothesis U2: (- dExp bo <= Fexp a + Fexp c - precision)%Z.
Hypothesis U3: (- dExp bo <= Fexp q - precision)%Z.
Hypothesis U4: (- dExp bo <= Fexp b + Fexp b' - precision)%Z.
Hypothesis U5: (- dExp bo <= (Fexp d)-1)%Z.


Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Ns:(Fnormal radix bo s).
Hypothesis Nd:(Fnormal radix bo d).

Hypothesis Square:(0 <=b*b')%R.

Hypothesis Roundp : (EvenClosest bo radix precision (b*b')%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).

Hypothesis p_pos:(0 <= p)%R.
Hypothesis q_pos:(0 <= q)%R.


Hypothesis Secondcase : (3*(Rabs (p-q)) < p+q)%R.

Hypothesis Roundt : (EvenClosest bo radix precision (p-q)%R t).
Hypothesis dpEq   : (FtoRradix dp=b*b'-p)%R.
Hypothesis dqEq   : (FtoRradix dq=a*c-q)%R.
Hypothesis Rounds : (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis Roundd : (EvenClosest bo radix precision (t+s)%R d).

Hypothesis p_differ_q:~(p=q)%R.

Variable e:Z.
Hypothesis p_eqF : p=(Float (Zpower_nat radix (pred precision)) (Zsucc e)).
Hypothesis p_eqR : (FtoRradix p)=(powerRZ radix (precision+e)%Z).
Hypothesis q_eqExp : (Fexp q)=e.


Theorem discri5: (0 < dp*dq)%R -> (delta <= 2*(Fulp bo radix precision d))%R.
intros.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
assert (forall f1 f2 g : float,
      Fbounded bo f1 ->
      Fbounded bo f2 ->
      Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
      (- dExp bo <= Fexp f1 + Fexp f2 - precision)%Z ->
      (- dExp bo <= Fexp g - precision)%Z ->
      Fcanonic 2 bo g ->
      exists s : float,
        Fbounded bo s /\
        FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
        Fexp s = (Fexp g - precision)%Z /\
        (Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'. 
exists (Fminus radix dp' dq'); split.
2: unfold FtoRradix; rewrite Fminus_correct; auto with real.
unfold Fminus, Fopp, Fplus; simpl.
repeat rewrite H4'; repeat rewrite q_eqExp; repeat rewrite H4.
replace (Fexp p) with (Zsucc e); [idtac|rewrite p_eqF; auto].
rewrite Zmin_le2; auto with zarith.
split; auto with zarith.
simpl; unfold Zsucc.
ring_simplify  (e + 1 - precision - (e - precision))%Z; 
  ring_simplify (e - precision - (e - precision))%Z.
simpl.
unfold nat_of_P, Zpower_nat; simpl.
replace ( - Fnum dq' * 1)%Z with  (- Fnum dq')%Z; [idtac|ring].
apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; rewrite plus_IZR;rewrite mult_IZR;rewrite Ropp_Ropp_IZR.
assert (forall (x y z:R), (0 < x*y)%R -> (Rabs x <= z)%R ->
   (Rabs y <= z)%R -> (Rabs (2*x-y) < 2*z)%R).
intros.
unfold Rabs; case (Rcase_abs (2*x-y)%R); case (Rle_or_lt 0%R x); intros.
case H7; intros;ring_simplify (- (2 * x - y))%R.
assert (-x <0)%R; auto with real.
apply Rlt_le_trans with (-2*0+y)%R; auto with real.
apply Rplus_lt_compat_r; repeat rewrite Ropp_mult_distr_l_reverse.
apply Ropp_lt_contravar; apply Rmult_lt_compat_l; auto with real.
ring_simplify (-2*0+y)%R; apply Rle_trans with z; auto with real.
apply Rle_trans with (2:=H6); apply RRle_abs.
apply Rle_trans with (1*z)%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with (2:=H1); auto with real.
Contradict H0; rewrite <- H8; auto with real.
ring_simplify (0*y)%R; auto with real.
ring_simplify (- (2 * x - y))%R.
apply Rlt_le_trans with ((-2*x)+0)%R;[apply Rplus_lt_compat_l|idtac].
apply Rmult_lt_reg_l with (-x)%R; auto with real.
apply Rle_lt_trans with (-(x*y))%R; auto with real.
apply Rlt_le_trans with (-0)%R; auto with real; right;ring.
apply Rle_trans with (2*(-x))%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rlt_le_trans with (2*x-0)%R;[unfold Rminus; apply Rplus_lt_compat_l|idtac].
apply Ropp_lt_contravar; apply Rmult_lt_reg_l with x; auto with real.
case H7; auto with real.
intros H8; Contradict H0; rewrite <- H8; ring_simplify (0*y)%R; auto with real.
ring_simplify (x*0)%R; auto with real.
apply Rle_trans with (2*x)%R;[right;ring|apply Rmult_le_compat_l; auto with real].
apply Rle_trans with (2:=H1); apply RRle_abs.
apply Rlt_le_trans with (2*0-y)%R; [unfold Rminus; apply Rplus_lt_compat_r; apply Rmult_lt_compat_l; auto with real|idtac].
apply Rle_trans with (-y)%R;[right;ring|apply Rle_trans with z].
apply Rle_trans with (2:=H6); rewrite <- Rabs_Ropp; apply RRle_abs.
apply Rle_trans with (1*z)%R;[right;ring|apply Rmult_le_compat_r; auto with real].
apply Rle_trans with (2:=H1); auto with real.
replace (Fnum dp' * Zpos 2+-Fnum dq')%R with (2*(Fnum dp')-Fnum dq')%R; auto with real zarith.
apply Rlt_le_trans with (2*powerRZ radix (Zpred precision))%R.
apply H0; auto.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dq')); auto with real zarith.
apply Rmult_lt_reg_l with (powerRZ radix (Fexp dp')); auto with real zarith.
apply Rle_lt_trans with 0%R;[right;ring|apply Rlt_le_trans with (1:=H)].
rewrite dpEq; rewrite dqEq; rewrite <- H3; rewrite <- H3'.
unfold FtoRradix, FtoR; right; ring.
right; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith. 
simpl; field; apply Rmult_integral_contrapositive; split; auto with real.
simpl; ring.
simpl;rewrite <-q_eqExp; rewrite <- H4'; auto with zarith float.
Qed.


Theorem discri6: (0< dp)%R -> (dq < 0)%R 
    -> (delta <= 2*(Fulp bo radix precision d))%R.
intros;unfold delta.
replace (d - (b * b' - a * c))%R with (-((t+s)-d)+-((dp-dq)-s))%R.
2: rewrite dpEq; rewrite dqEq; unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto; ring.
apply Rle_trans with (1:=Rabs_triang (-(t+s-d))%R (-(dp-dq-s))%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith;rewrite Rmult_plus_distr_l.
apply Rle_trans with ((Fulp bo radix precision d)+(Fulp bo radix precision s))%R;[apply Rplus_le_compat|idtac].
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundd; auto.
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Rounds; auto. 
apply Rle_trans with ((Fulp bo radix precision d+ 3* Fulp bo radix precision d))%R;[apply Rplus_le_compat_l|simpl;right;ring].
apply Rle_trans with (2*Fulp bo radix precision d)%R;[idtac|unfold Fulp; auto with real zarith].
rewrite FulpFabs; auto; rewrite FulpFabs with bo radix precision d; auto.
assert (2*(Fabs d)=(Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d)))))%R.
unfold FtoRradix, FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith;  simpl; ring.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum (Fabs d)) (Zsucc (Fexp (Fabs d))))).
2:assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac]. 
2:right; rewrite CanonicFulp; auto; [rewrite CanonicFulp|left]; auto.
2:unfold FtoR, Zsucc; simpl; rewrite powerRZ_add; auto with real zarith.
2:simpl; ring.
2:left; auto.
2:elim H2; intros H6 H5; elim H6; intros.
2:split; simpl; auto with zarith.
2:split; simpl; auto with zarith.
apply LeFulpPos; auto with real float.
assert (Fnormal radix bo (Fabs d));[apply FnormalFabs; auto|idtac].
elim H2; intros H6 H5; elim H6; intros;split; simpl; auto with zarith.
rewrite Fabs_correct; auto with real zarith.
apply EvenClosestMonotone2 with bo precision (Rabs (dp-dq))%R (2*Rabs (t+s))%R; auto.
2: apply EvenClosestFabs; auto; left; auto.
2: apply Twice_EvenClosest_Round; auto.
2: apply FnormalFabs; auto.
2: apply EvenClosestFabs; auto; left; auto.
unfold Rminus; apply Rle_trans with (1:=Rabs_triang dp (-dq)%R).
apply Rmult_le_reg_l with (INR 2); auto with real zarith; rewrite Rmult_plus_distr_l.
apply Rle_trans with (Fulp bo radix precision p+Fulp bo radix precision q)%R;[apply Rplus_le_compat|idtac].
rewrite dpEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite Rabs_Ropp; rewrite dqEq; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
rewrite CanonicFulp; auto with float;[idtac|left; auto].
rewrite CanonicFulp; auto with float;[idtac|left; auto].
apply Rle_trans with (3*(powerRZ radix e))%R;[right|idtac].
unfold FtoRradix, FtoR; simpl; rewrite q_eqExp; rewrite p_eqF; simpl.
unfold Zsucc; rewrite powerRZ_add; auto with real zarith; simpl;ring.
assert ((powerRZ radix e <= t))%R.
unfold FtoRradix, radix; rewrite t_exact with bo precision b b' p q t; auto.
fold radix; fold FtoRradix; rewrite p_eqR.
apply Rle_trans with (powerRZ radix (precision + e) - ((powerRZ radix precision - 1) * powerRZ radix e))%R; auto with real.
rewrite powerRZ_add; auto with real zarith; right;ring.
unfold Rminus; apply Rplus_le_compat_l; auto with real.
apply Ropp_le_contravar.
unfold FtoRradix, FtoR; rewrite q_eqExp; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=(RRle_abs (Fnum q))).
assert (Zabs (Fnum q) < Zpower_nat radix precision)%Z; auto with real zarith float.
rewrite <- pGivesBound; auto with zarith float.
rewrite Rabs_Zabs; apply Rle_trans with (Zpred (Zpower_nat radix precision)); auto with real zarith.
unfold Zpred; rewrite plus_IZR.
rewrite Zpower_nat_Z_powerRZ; right; simpl; ring.
assert (0<=s)%R.
unfold FtoRradix; apply RleRoundedR0 with bo precision (EvenClosest bo radix precision) (dp-dq)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Rle_trans with (0-0)%R; unfold Rminus; auto with real.
apply Rplus_le_compat; auto with real.
rewrite Rabs_right; auto with real.
2: apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.
2: apply Rplus_le_compat; auto with real zarith.
2: apply Rle_trans with (2:=H2); auto with real zarith.
apply Rle_trans with (4*powerRZ radix e)%R;[apply Rmult_le_compat_r; auto with real zarith|idtac].
replace 3%R with (INR 3);[idtac|simpl; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (4*(t+s))%R;[apply Rmult_le_compat_l; auto with real|simpl; right; ring].
replace 4%R with (INR 4);[auto with real zarith|simpl;ring].
apply Rle_trans with (powerRZ radix e+0)%R;[idtac|apply Rplus_le_compat];auto with real.
Qed.



Theorem discri7: (dp < 0)%R -> (0 < dq)%R 
    -> (delta <= 2*(Fulp bo radix precision d))%R.
intros L1 L2.
unfold delta, FtoRradix; apply discri3 with p q t dp dq s; auto.
assert (H0:forall f1 f2 g : float,
      Fbounded bo f1 ->
      Fbounded bo f2 ->
      Closest bo 2 (FtoR 2 f1 * FtoR 2 f2) g ->
      (- dExp bo <= Fexp f1 + Fexp f2 - precision)%Z ->
      (- dExp bo <= Fexp g - precision)%Z ->
      Fcanonic 2 bo g ->
      exists s : float,
        Fbounded bo s /\
        FtoR 2 s = (FtoR 2 f1 * FtoR 2 f2 - FtoR 2 g)%R /\
        Fexp s = (Fexp g - precision)%Z /\
        (Rabs (Fnum s) <= powerRZ (Zpos 2) (Zpred precision))%R).
apply errorBoundedMultClosest_Can; auto.
fold radix in H0; fold FtoRradix in H0.
elim H0 with (f1:=b) (f2:=b') (g:=p); auto with zarith real.
intros dp' T2; elim T2; intros H2 T3; elim T3; intros H3 T4; elim T4; intros H4 
H5; clear T2 T3 T4.
2: elim Roundp; auto.
elim H0 with (f1:=a) (f2:=c) (g:=q); auto with zarith real; clear H0.
intros dq' T2; elim T2; intros H2' T3; elim T3; intros H3' T4; elim T4; intros H4' H5'; clear T2 T3 T4.
2: elim Roundq; auto.
2: left; auto.
2: left; auto.
cut (exists dp'':float, (Fexp dp''=Fexp dq' /\ (FtoRradix dp''=dp')%R /\
  (Rabs (Fnum dp'') <= powerRZ radix (Zpred precision))%R)).
intros T; elim T; intros dp'' T1; elim T1; intros H4'' T2; elim T2;
 intros H5'' H6''; clear T T1 T2.
assert ((Rabs (Fnum dp''-Fnum dq') < (powerRZ radix precision))%R \/ 
 (((Rabs dp'')= (powerRZ radix (Zpred (Fexp q))))%R /\  ((Rabs dq')=     
(powerRZ radix (Zpred (Fexp q))))%R)).
case H6''; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') 
(-(Fnum dq'))%R).
rewrite Rabs_Ropp.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum 
dq')))%R; auto with real zarith.
apply Rle_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix 
(Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
case H5'; intros.
left; unfold Rminus; apply Rle_lt_trans with (1:=Rabs_triang (Fnum dp'') (-(Fnum 
dq'))%R); rewrite Rabs_Ropp.
apply Rle_lt_trans with ((powerRZ radix (Zpred precision)) +(Rabs (Fnum dq')))%R
; auto with real zarith.
apply Rlt_le_trans with ((powerRZ radix (Zpred precision))+ (powerRZ radix (Zpred precision)))%R; auto with real zarith.
right; unfold Zpred; repeat rewrite powerRZ_add; auto with real zarith.
simpl; field.
right; unfold FtoRradix, FtoR;repeat rewrite Rabs_mult.
rewrite (Rabs_right (powerRZ radix (Fexp dp''))); try apply Rle_ge; auto with real zarith.
rewrite (Rabs_right (powerRZ radix (Fexp dq'))); try apply Rle_ge; auto with real zarith.
rewrite H; rewrite H0.
repeat rewrite <- powerRZ_add; auto with real zarith.
rewrite H4''; rewrite H4'; unfold Zpred.
ring_simplify (precision + -1 + (Fexp q - precision))%Z; 
  ring_simplify (precision + -1 + (Fexp q - precision))%Z; 
    ring_simplify (Fexp q+-1)%Z; auto with zarith real.
case H; intros V; clear H.
exists (Float (Fnum dp''-Fnum dq') (Fexp dq')).
split;[split; auto with zarith|idtac].
simpl; apply Zlt_Rlt.
rewrite pGivesBound;rewrite Zpower_nat_Z_powerRZ; auto.
rewrite <- Rabs_Zabs; unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith.
simpl; auto with zarith float.
fold radix; fold FtoRradix; rewrite dpEq; rewrite dqEq.
rewrite <- H3'; rewrite <- H3;rewrite <- H5''.
unfold FtoRradix, FtoR; simpl.
unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR.
rewrite H4''; ring.
exists (Float (-1)%Z (Fexp q)).
split;[split; simpl; auto with zarith|idtac].
rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
fold radix; fold FtoRradix; elim V; intros.
replace (FtoRradix dp) with (-(-dp))%R;[idtac|ring].
rewrite <- (Rabs_left dp); auto with real.
rewrite <- (Rabs_right dq); auto with real.
2: apply Rle_ge; auto with real.
rewrite dpEq; rewrite <- H3; rewrite <- H5''; rewrite H.
rewrite dqEq; rewrite <- H3'; rewrite H0.
unfold FtoRradix, FtoR, Zpred; simpl.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
assert (FtoRradix dp'=(Float (2*Fnum dp') (Zpred (Fexp dp'))))%R.
unfold FtoRradix, FtoR, Zpred.
apply trans_eq with ((2 * Fnum dp')%Z*(powerRZ radix (Fexp dp'+-1)))%R;[auto|idtac].
rewrite mult_IZR;rewrite powerRZ_add; auto with real zarith; simpl; field.
simpl; auto with real.
exists (Float (2*Fnum dp') (Zpred (Fexp dp'))); split.
simpl; rewrite H4'; rewrite H4.
rewrite q_eqExp; rewrite p_eqF; unfold Zpred, Zsucc;simpl; auto with zarith.
split; auto with real.
apply Rmult_le_reg_l with (powerRZ radix (Zpred (Fexp dp'))); auto with real zarith.
rewrite <- powerRZ_add; auto with real zarith.
rewrite <- (Rabs_right (powerRZ radix (Zpred (Fexp dp'))));auto with real.
2: apply Rle_ge; auto with real zarith.
rewrite <- Rabs_mult.
replace (powerRZ radix (Zpred (Fexp dp')) *
  Fnum (Float (2 * Fnum dp') (Zpred (Fexp dp'))))%R with (FtoRradix dp'); auto with real.
2: rewrite H; unfold FtoRradix, FtoR; simpl; auto with real.
rewrite H3; rewrite <- dpEq.
rewrite H4; unfold Zpred;ring_simplify (Fexp p - precision + -1 + (precision + -1))%Z.
rewrite Rabs_left; auto with real.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rplus_le_reg_l with (FtoRradix dp).
ring_simplify (dp+2*(-dp))%R.
rewrite <- Rabs_left; auto with real.
assert (Fbounded bo (Float (Zpred (Zpower_nat radix precision)) e)).
split; auto with zarith.
simpl; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
simpl; auto with zarith.
rewrite <- Rabs_Ropp.
replace (-dp)%R with (p-b*b')%R; [idtac|rewrite dpEq;ring].
elim Roundp; intros K1 K2; elim K1; intros K3 K4.
apply Rle_trans with (Rabs ((Float (Zpred (Zpower_nat radix precision)) e)-b*b')).
unfold FtoRradix; apply K4; auto.
clear K1 K2 K3 K4; rewrite Rabs_left1.
rewrite dpEq; rewrite p_eqR.
apply Rle_trans with (b*b'-(powerRZ radix precision -1)*(powerRZ radix e))%R.
unfold FtoRradix, FtoR, Zpred, radix; simpl.
rewrite plus_IZR; simpl; right; ring_simplify.
rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring.
unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
ring_simplify (e+1-2)%Z; unfold Zminus.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Rplus_le_reg_l with (p-(Float (Zpred (Zpower_nat radix precision)) e))%R.
apply Rle_trans with (-(b*b'-p))%R;[right;ring|idtac].
rewrite <- dpEq; rewrite <- Rabs_left; auto with real.
rewrite dpEq; apply Rmult_le_reg_l with (INR 2); auto with real zarith.
apply Rle_trans with (Fulp bo radix precision p).
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
rewrite CanonicFulp; auto;[idtac|left; auto].
replace (Fexp p) with (Zsucc e);[unfold Zsucc|rewrite p_eqF; simpl; auto with zarith].
rewrite p_eqR; unfold FtoRradix, FtoR, Zpred; simpl.
rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
Qed.

Theorem discri8: (delta <= 2*(Fulp bo radix precision d))%R.
case (Rle_or_lt 0%R dp); intros H;[case H; clear H; intros H|idtac].
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri5; auto with real.
apply Rle_lt_trans with (dp*0)%R;[right;ring|auto with real].
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri6; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists (Fopp dq); split; auto with float zarith.
rewrite Fopp_correct; fold radix; fold FtoRradix; rewrite <- H; ring.
case (Rle_or_lt 0%R dq); intros H';[case H'; clear H'; intros H'|idtac].
apply discri7; auto.
unfold FtoRradix, delta; apply discri3 with p q t dp dq s; auto.
exists dp; split; auto.
fold radix; fold FtoRradix; rewrite <- H'; ring.
apply discri5; auto.
apply Rle_lt_trans with (-dp*0)%R;[right;ring|idtac].
apply Rlt_le_trans with ((-dp)*(-dq))%R;[auto with real|right;ring].
Qed.

End Discriminant3.

Section Discriminant4.
Variable bo : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.

Variables a b c p q t dp dq s d:float.

Let delta := (Rabs (d-(b*b-a*c)))%R.

Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).

(** There is no underflow *)
Hypothesis U0: (- dExp bo <= Fexp d - 1)%Z.
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (- dExp bo <= Fexp a + Fexp c - precision)%Z.
Hypothesis U3: (- dExp bo <= Fexp q - precision)%Z.
Hypothesis U4: (- dExp bo <= Fexp b + Fexp b - precision)%Z.
Hypothesis U5: (- dExp bo <= Fexp p - precision)%Z.

Hypothesis Np:(Fnormal radix bo p).
Hypothesis Nq:(Fnormal radix bo q).
Hypothesis Ns:(Fnormal radix bo s).
Hypothesis Nd:(Fnormal radix bo d).

Hypothesis Roundp : (EvenClosest bo radix precision (b*b)%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).

Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R -> 
   (EvenClosest bo radix precision (p-q)%R d).

Hypothesis SRoundt : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (p-q)%R t).
Hypothesis SdpEq   : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dp=b*b-p)%R.
Hypothesis SdqEq   : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dq=a*c-q)%R.
Hypothesis SRounds : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis SRoundd : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (t+s)%R d).

Theorem discri9: (delta <= 2*(Fulp bo radix precision d))%R.
assert (Square:(0<=b*b)%R).
apply Rle_trans with (Rsqr b); auto with real.
case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros. 
unfold delta;apply discri1 with p q; auto.
case (Rle_or_lt (3*(Rmin (Fulp bo radix precision p) (Fulp bo radix precision q)))%R (Rabs (p-q))%R); intros.
unfold delta; apply discri2 with p q t dp dq s; auto.
case (Zle_or_lt (Fexp q) (Fexp p)); intros.
case (Zle_lt_or_eq (Fexp q) (Fexp p)); auto;intros.
assert (Fexp q = Zpred (Fexp p))%Z.
cut (Zle (Fexp q) (Zpred (Fexp p))); auto with zarith.
cut (Zle (Zpred (Fexp p)) (Fexp q)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum p) (Zpred (Fexp p)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
simpl; elim Np; auto with zarith.
apply Rle_trans with (Fulp bo radix precision q).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply P_positive with bo precision b b; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix p).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply P_le_two_Q with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1 H2; assert (FtoRradix p=powerRZ radix (precision+Zpred (Fexp p)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum p)).
elim Np; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H2).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum p)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply P_positive with bo precision b b; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H3; unfold Rmin.
case (Rle_dec (powerRZ radix (Fexp p)) (powerRZ radix (Zpred (Fexp p)))); auto with real zarith; intros J.
Contradict J; apply Rlt_not_le; auto with real zarith.
clear J; rewrite Rabs_right.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with ((Zsucc (Zpower_nat radix (pred precision))*(powerRZ radix (Fexp p))+-((Zpred (Zpower_nat radix precision))*(powerRZ radix (Fexp q)))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H3; unfold Zpred; simpl; right;ring_simplify.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum q)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fq; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rle_ge; apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp p)%Z with (precision + Zpred (Fexp p))%Z;[auto with real|unfold Zpred; ring].
unfold delta; apply discri8 with p q t dp dq s (Zpred (Fexp p)); auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp p))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp p + -1 + 1))%Z with (precision+(Fexp p+-1))%Z; auto with real; ring.
unfold delta;apply discri4 with p q t dp dq s; auto.
assert (Fexp p = Zpred (Fexp q))%Z.
cut (Zle (Fexp p) (Zpred (Fexp q))); auto with zarith.
cut (Zle (Zpred (Fexp q)) (Fexp p)); auto with zarith.
clear H1;apply Zle_powerRZ with radix; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision (Float (Fnum q) (Zpred (Fexp q)))).
rewrite CanonicFulp; auto.
unfold FtoR; simpl; right; ring.
left; split; auto with zarith.
split; simpl; auto with zarith float.
simpl; elim Nq; auto with zarith.
apply Rle_trans with (Fulp bo radix precision p).
apply LeFulpPos; auto with real float zarith.
split; simpl; auto with zarith float.
apply LeFnumZERO; simpl; auto with real zarith.
apply LeR0Fnum with radix; auto with real zarith.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply Rmult_le_reg_l with 2%R; auto with real.
apply Rle_trans with (FtoRradix q).
unfold FtoRradix, FtoR, Zpred; simpl; rewrite powerRZ_add; auto with real zarith; simpl; right; field.
apply Q_le_two_P with bo precision b b; auto.
rewrite CanonicFulp; auto with zarith.
unfold FtoR; simpl; right; ring.
left; auto.
clear H1; assert (FtoRradix q=powerRZ radix (precision+Zpred (Fexp q)))%R.
case (Zle_lt_or_eq (Zpower_nat radix (pred precision)) (Fnum q)).
elim Nq; intros.
apply Zmult_le_reg_r with radix; auto with zarith.
apply Zlt_gt; auto with zarith.
apply Zle_trans with (Zpower_nat radix precision).
pattern radix at 2 in |-*; replace radix with (Zpower_nat radix 1).
rewrite <- Zpower_nat_is_exp; auto with zarith.
simpl; auto with zarith.
rewrite <- pGivesBound; apply Zle_trans with (1:=H3).
rewrite Zabs_eq; auto with zarith.
cut (0<=Fnum q)%Z; auto with zarith.
apply LeR0Fnum with radix; auto.
apply Rlt_le; apply Q_positive with bo precision b b p; auto.
intros H1; Contradict H0.
apply Rle_not_lt.
rewrite CanonicFulp; auto; [idtac|left; auto].
rewrite CanonicFulp; auto; [idtac|left; auto].
replace (FtoR radix (Float (S 0) (Fexp p))) with (powerRZ radix (Fexp p));[idtac|unfold FtoR; simpl; ring].
replace (FtoR radix (Float (S 0) (Fexp q))) with (powerRZ radix (Fexp q));[idtac|unfold FtoR; simpl; ring].
rewrite H2; unfold Rmin.
case (Rle_dec (powerRZ radix (Zpred (Fexp q))) (powerRZ radix (Fexp q))); auto with real zarith; intros J.
clear J; rewrite Rabs_left1.
unfold FtoRradix, FtoR, Rminus.
apply Rle_trans with  (- ((Zpred (Zpower_nat radix precision)) * powerRZ radix (Fexp p) + - ((Zsucc (Zpower_nat radix (pred precision))) * powerRZ radix (Fexp q))))%R.
unfold Zpred, Zsucc; rewrite plus_IZR; rewrite plus_IZR; repeat rewrite Zpower_nat_Z_powerRZ.
rewrite inj_pred; auto with zarith.
rewrite H2; unfold Zpred; simpl; right;ring_simplify.
repeat rewrite powerRZ_add; auto with real zarith; simpl; field.
apply Ropp_le_contravar.
apply Rplus_le_compat;[apply Rmult_le_compat_r; auto with real zarith|idtac].
2:apply Ropp_le_contravar; apply Rmult_le_compat_r; auto with real zarith.
apply Rle_trans with (1:=RRle_abs (Fnum p)).
rewrite Rabs_Zabs; rewrite <- pGivesBound;auto with zarith float.
elim Fp; intros; auto with zarith.
apply Rle_IZR;apply Zle_Zpred; auto.
apply Rlt_le; apply Rplus_lt_reg_r with q.
ring_simplify.
unfold FtoRradix; apply FcanonicPosFexpRlt with bo precision; auto with zarith.
2:apply Rlt_le; apply Q_positive with bo precision b b p; auto.
apply P_positive with bo precision b b; auto.
left; auto.
left; auto.
Contradict J; auto with real zarith.
intros H1; unfold FtoRradix, FtoR; rewrite <- H1.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith.
replace (Zpred precision+Fexp q)%Z with (precision + Zpred (Fexp q))%Z;[auto with real|unfold Zpred; ring].
unfold delta; rewrite <-Rabs_Ropp.
replace (- (d - (b * b - a * c)))%R with (Fopp d-(a*c-b*b))%R;[idtac|unfold FtoRradix; rewrite Fopp_correct; ring].
replace (Fulp bo radix precision d) with (Fulp bo radix precision (Fopp d)); auto with float zarith.
2: unfold Fulp; rewrite Fnormalize_Fopp; unfold Fopp; simpl; auto with real zarith.
apply discri8 with q p (Fopp t) dq dp (Fopp s) (Zpred (Fexp q)); auto with float zarith.
apply FnormalFop; auto.
apply FnormalFop; auto.
fold radix; fold FtoRradix; case (Rle_or_lt 0%R (a*c)%R); auto.
intros H3; absurd (0 < q)%R.
apply Rle_not_lt; unfold FtoRradix; apply RleRoundedLessR0 with bo precision (EvenClosest bo radix precision) (a*c)%R; auto with real.
apply EvenClosestRoundedModeP; auto.
apply Q_positive with bo precision b b p; auto.
fold radix; fold FtoRradix; rewrite (Rplus_comm q p).
replace (q-p)%R with (-(p-q))%R; auto with real; rewrite Rabs_Ropp; auto.
fold radix; fold FtoRradix; replace (q-p)%R with (-(p-q))%R; auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (dq-dp)%R with (-(dp-dq))%R;auto with real.
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
fold radix; fold FtoRradix; replace (Fopp t+Fopp s)%R with (-(t+s))%R;[idtac|unfold FtoRradix; repeat rewrite Fopp_correct; ring].
generalize EvenClosestSymmetric; unfold SymmetricP;intros T; apply T; auto.
apply FcanonicUnique with radix bo precision; auto with zarith real.
left; auto.
left; split; [split;simpl|idtac]; auto with zarith.
rewrite Zabs_eq; auto with zarith.
rewrite pGivesBound; auto with zarith.
simpl (Fnum (Float (Zpower_nat 2 (pred precision)) (Zsucc (Zpred (Fexp q))))).
replace radix with (Zpower_nat radix 1);[idtac|simpl; auto with zarith].
rewrite <-Zpower_nat_is_exp; rewrite pGivesBound; auto with zarith.
rewrite Zabs_eq; auto with zarith.
fold FtoRradix; rewrite H1; unfold FtoRradix, FtoR, Zpred, Zsucc; simpl.
rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.
rewrite inj_pred; auto with zarith; unfold Zpred.
replace (precision + -1 + (Fexp q + -1 + 1))%Z with (precision+(Fexp q+-1))%Z; auto with real; ring.
Qed.

End Discriminant4.


Section Discriminant5.
Variable bo : Fbound.
Variable precision : nat.
 
Let radix := 2%Z.

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

Let radixMoreThanZERO := Zlt_1_O _ (Zlt_le_weak _ _ TwoMoreThanOne).
Hint Resolve radixMoreThanZERO: zarith.
Hypothesis precisionGreaterThanOne : 1 < precision.
Hypothesis pGivesBound : Zpos (vNum bo) = Zpower_nat radix precision.

Variables a b c p q t dp dq s d:float.

Let delta := (Rabs (d-(b*b-a*c)))%R.

Hypothesis Fa : (Fbounded bo a).
Hypothesis Fb : (Fbounded bo b).
Hypothesis Fc : (Fbounded bo c).
Hypothesis Fp : (Fbounded bo p).
Hypothesis Fq : (Fbounded bo q).
Hypothesis Fd : (Fbounded bo d).
Hypothesis Ft : (Fbounded bo t).
Hypothesis Fs : (Fbounded bo s).
Hypothesis Fdp: (Fbounded bo dp).
Hypothesis Fdq: (Fbounded bo dq).

(** There is no underflow *)
Hypothesis U0: (- dExp bo <= Fexp d - 1)%Z.
Hypothesis U1: (- dExp bo <= (Fexp t)-1)%Z.
Hypothesis U2: (- dExp bo <= Fexp a + Fexp c - precision)%Z.
Hypothesis U3: (- dExp bo <= Fexp q - precision)%Z.
Hypothesis U4: (- dExp bo <= Fexp b + Fexp b - precision)%Z.
Hypothesis U5: (- dExp bo <= Fexp p - precision)%Z.

Hypothesis Np:(FtoRradix p=0)%R \/ (Fnormal radix bo p).
Hypothesis Nq:(FtoRradix q=0)%R \/ (Fnormal radix bo q). 
Hypothesis Ns:(FtoRradix s=0)%R \/ (Fnormal radix bo s).
Hypothesis Nd: (Fnormal radix bo d).

Hypothesis Roundp : (EvenClosest bo radix precision (b*b)%R p).
Hypothesis Roundq : (EvenClosest bo radix precision (a*c)%R q).

Hypothesis Firstcase : (p+q <= 3*(Rabs (p-q)))%R -> 
   (EvenClosest bo radix precision (p-q)%R d).

Hypothesis SRoundt : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (p-q)%R t).
Hypothesis SdpEq   : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dp=b*b-p)%R.
Hypothesis SdqEq   : (3*(Rabs (p-q)) < p+q)%R -> (FtoRradix dq=a*c-q)%R.
Hypothesis SRounds : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (dp-dq)%R s).
Hypothesis SRoundd : (3*(Rabs (p-q)) < p+q)%R -> (EvenClosest bo radix precision (t+s)%R d).

Theorem discri: (delta <= 2*(Fulp bo radix precision d))%R.
case Np; intros.
assert (FtoRradix d=(Fopp q))%R.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with float zarith.
replace (FtoR radix (Fopp q)) with (p-q)%R; [apply Firstcase|rewrite Fopp_correct; fold FtoRradix; rewrite H; ring].
rewrite H; ring_simplify (0-q)%R; ring_simplify (0+q)%R.
rewrite Rabs_Ropp; apply Rle_trans with (1:=(RRle_abs q)).
apply Rle_trans with (1*(Rabs q))%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with 2%R; auto with real.
unfold delta; rewrite H0.
unfold FtoRradix; rewrite Fopp_correct; fold FtoRradix.
replace (-q-(b*b-a*c))%R with ((a*c-q)+(-(b*b)))%R;[idtac|ring].
apply Rle_trans with (1:=(Rabs_triang (a * c - q)%R (-(b*b))%R)).
apply Rle_trans with (/2*(Fulp bo radix precision q)+/2*(Fulp bo radix precision p))%R.
apply Rplus_le_compat; apply Rmult_le_reg_l with (2%nat)%R; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision q);[idtac|simpl; right; field; auto with real].
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
apply Rle_trans with (Fulp bo radix precision p);[idtac|simpl; right; field; auto with real].
replace (-(b*b))%R with (-(b*b-p))%R;[rewrite Rabs_Ropp|rewrite H;ring].
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
apply Rle_trans with (/ 2 * Fulp bo radix precision q + / 2 * Fulp bo radix precision q)%R;[apply Rplus_le_compat; auto with real|idtac].
apply Rmult_le_compat_l; auto with real.
rewrite Fulp_zero.
unfold Fulp; apply Rle_powerRZ;auto with real zarith float.
apply is_Fzero_rep2 with radix; auto with zarith.
apply Rle_trans with (1 * Fulp bo radix precision q)%R;[right; field; auto with real|idtac].
apply Rmult_le_compat; auto with real zarith float.
unfold Fulp; auto with real zarith.
right; apply trans_eq with (Fulp bo radix precision (Fopp q)).
unfold Fulp; rewrite Fnormalize_Fopp; auto with real zarith.
apply FulpComp; auto with float zarith.
case Nq; intros.
assert (FtoRradix d=p)%R.
apply sym_eq; unfold FtoRradix; apply RoundedModeProjectorIdemEq with bo precision (EvenClosest bo radix precision); auto with float zarith.
replace (FtoR radix p) with (p-q)%R; [apply Firstcase|fold FtoRradix; rewrite H0; ring].
rewrite H0; ring_simplify (p+0)%R; ring_simplify (p-0)%R.
apply Rle_trans with (1:=(RRle_abs p)).
apply Rle_trans with (1*(Rabs p))%R; auto with real.
apply Rmult_le_compat_r; auto with real.
apply Rle_trans with 2%R; auto with real.
unfold delta; rewrite H1.
replace (p-(b*b-a*c))%R with (a*c+(-(b*b-p)))%R;[idtac|ring].
apply Rle_trans with (1:=(Rabs_triang (a * c )%R (-(b*b-p))%R)).
apply Rle_trans with (/2*(Fulp bo radix precision q)+/2*(Fulp bo radix precision p))%R.
apply Rplus_le_compat; apply Rmult_le_reg_l with (2%nat)%R; auto with real zarith.
apply Rle_trans with (Fulp bo radix precision q);[idtac|simpl; right; field; auto with real].
replace (a*c)%R with (a*c-q)%R;[idtac|rewrite H0;ring].
unfold FtoRradix; apply ClosestUlp; auto.
elim Roundq; auto.
apply Rle_trans with (Fulp bo radix precision p);[idtac|simpl; right; field; auto with real].
rewrite Rabs_Ropp; unfold FtoRradix; apply ClosestUlp; auto.
elim Roundp; auto.
apply Rle_trans with (/ 2 * Fulp bo radix precision p + / 2 * Fulp bo radix precision p)%R;[apply Rplus_le_compat; auto with real|idtac].
apply Rmult_le_compat_l; auto with real.
rewrite Fulp_zero.
unfold Fulp; apply Rle_powerRZ;auto with real zarith float.
apply is_Fzero_rep2 with radix; auto with zarith.
apply Rle_trans with (1 * Fulp bo radix precision p)%R;[right; field; auto with real|idtac].
apply Rmult_le_compat; auto with real zarith float.
unfold Fulp; auto with real zarith.
right; apply FulpComp; auto with float zarith.
case (Rle_or_lt (p + q)%R (3 * Rabs (p - q))%R); intros. 
unfold delta;apply discri1 with p q; auto.
apply Rle_trans with (Rsqr (FtoR 2 b)) ; auto with real.
case Ns; intros.
unfold delta; apply discri3 with p q t dp dq s; auto with real float zarith.
apply Rle_trans with (Rsqr (FtoR 2 b)) ; auto with real.
2:unfold delta; apply discri9 with p q t dp dq s; auto.
exists (Float 0%Z 0%Z).
split.
unfold Fbounded; split; auto with zarith.
simpl; case (dExp bo); auto with zarith.
apply trans_eq with 0%R.
unfold FtoR; simpl; ring.
fold radix; fold FtoRradix.
rewrite <- H2.
unfold FtoRradix; rewrite plusExactR0 with bo radix precision dp (Fopp dq) s; auto.
rewrite Fopp_correct; ring.
auto with zarith float.
replace (FtoR radix dp + FtoR radix (Fopp dq))%R with (dp - dq)%R; auto. 
elim SRounds; auto.
unfold FtoRradix; rewrite Fopp_correct; auto with real.
Qed.
End Discriminant5.