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