proposition: Lemma eqEqual: (Fexp q=s+Fexp x)%Z \/ ((FtoRradix q= - powerRZ radix (t+s+Fexp x))%R /\ (Rabs (x - hx) <= (powerRZ radix (s + Fexp x))/2)%R).
proof: Proof. generalize eqLe; generalize eqGe; intros. case H0; auto. intros; left; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz