proposition: Theorem maxMax1 : forall (p : float) (z : Z), Fbounded b p -> (Fexp p <= z)%Z -> (Fabs p <= Float (pPred (vNum b)) z)%R.
proof: Proof. intros p z H H0; unfold FtoRradix in |- *. rewrite <- (FshiftCorrect _ radixMoreThanOne (Z.abs_nat (z - Fexp p)) (Float (pPred (vNum b)) z)). unfold FtoR, Fabs in |- *; simpl in |- *; auto with zarith. rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ; auto with zarith. repeat rewrite inj_abs; auto with zarith. replace (z - (z - Fexp p))%Z with (Fexp p); [ idtac | ring ]. rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith. replace (z - Fexp p + Fexp p)%Z with z; [ idtac | ring ]. apply Rle_trans with (pPred (vNum b) * powerRZ radix (Fexp p))%R. apply Rle_monotone_exp; auto with zarith; repeat rewrite Rmult_IZR; apply IZR_le; unfold pPred in |- *; apply Zle_Zpred; auto with real zarith. apply H. apply Rmult_le_compat_l; auto with real zarith. apply IZR_le; unfold pPred in |- *; apply Zle_Zpred; auto with zarith. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz