proposition: Theorem FboundedMboundPos : forall z m : Z, (0 <= m)%Z -> (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' H'0 H'1; case (Zle_lt_or_eq _ _ H'0); intros H'2. exists (Float m z); split; auto with zarith. repeat split; simpl in |- *; lia. case (FboundNext (Float (Z.pred (Zpos (vNum b))) z)). split; auto with zarith. unfold Fnum. lia. intros f' (H1, H2); exists f'; split; auto. rewrite H2; rewrite pGivesBound. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto. rewrite <- Zsucc_pred; rewrite <- H'2; auto; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz