proposition: Theorem FboundedMbound2 : (0 < p) -> forall z m : Z, (Z.abs m <= Zpower_nat radix p)%Z -> (- dExp b <= z)%Z -> exists c : float, Fbounded b c /\ c = (m * powerRZ radix z)%R :>R /\ (z <= Fexp c)%Z.
proof: Proof. intros C z m H H0. case (Zle_or_lt 0 m); intros H1. case (FboundedMbound2Pos C z (Z.abs m)); auto; try rewrite Z.abs_eq; auto. intros f (H2, H3); exists f; split; auto. case (FboundedMbound2Pos C z (Z.abs m)); auto; try rewrite Zabs_eq_opp; auto with zarith. intros f (H2, H3); elim H3; intros; exists (Fopp f); split; auto with zarith. apply oppBounded; auto with zarith. split;[idtac|simpl; auto]. rewrite (Fopp_correct radix); auto with arith; fold FtoRradix in |- *; rewrite H4. rewrite Ropp_Ropp_IZR; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz