proposition: Theorem maxMaxBis : forall (p : float) (z : Z), Fbounded b p -> (Fexp p < z)%Z -> (Fabs p < Float nNormMin z)%R.
proof: Proof. intros p z H' H'0; apply Rlt_le_trans with (FtoR radix (Float (Zpos (vNum b)) (Z.pred z))). unfold FtoRradix in |- *; apply maxMax; auto with zarith; unfold Z.pred in |- *; auto with zarith. unfold FtoRradix, FtoR, nNormMin in |- *; simpl in |- *. pattern z at 2 in |- *; replace z with (Z.succ (Z.pred z)); [ rewrite powerRZ_Zs; auto with real zarith | unfold Z.succ, Z.pred in |- *; ring ]. rewrite <- Rmult_assoc. apply Rmult_le_compat_r; auto with real arith. apply powerRZ_le, IZR_lt; lia. pattern radix at 2 in |- *; rewrite <- (Zpower_nat_1 radix). rewrite <- mult_IZR. rewrite <- Zpower_nat_is_exp. replace (pred precision + 1) with precision. rewrite pGivesBound. apply Rle_refl. auto with zarith. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz