proposition: Theorem FboundedMbound2Pos : (0 < p) -> forall z m : Z, (0 <= m)%Z -> (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' 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. exists (Float 1 (p+z)). split;[split; simpl; auto with zarith|split]. rewrite pGivesBound; apply Z.le_lt_trans with (Zpower_nat radix 0); auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. unfold FtoRradix, FtoR; simpl; rewrite H'2; rewrite Zpower_nat_Z_powerRZ. rewrite powerRZ_add; auto with real zarith. apply IZR_neq; lia. simpl; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz