proposition: Theorem maxMax : forall (b : Fbound) (p : float) (z : Z), Fbounded b p -> (Fexp p <= z)%Z -> (Fabs p < Float (Zpos (vNum b)) z)%R.
proof: Proof. intros b p z H' H'0; unfold FtoRradix in |- *; rewrite <- (FshiftCorrect _ radixMoreThanOne (Z.abs_nat (z - Fexp p)) (Float (Zpos (vNum b)) z)); unfold Fshift in |- *. change (FtoR radix (Fabs p) < FtoR radix (Float (Zpos (vNum b) * Zpower_nat radix (Z.abs_nat (z - Fexp p))) (z - Z.abs_nat (z - Fexp p))))%R in |- *. replace (z - Z.abs_nat (z - Fexp p))%Z with (Fexp p). unfold Fabs, FtoR in |- *. change (Z.abs (Fnum p) * powerRZ radix (Fexp p) < (Zpos (vNum b) * Zpower_nat radix (Z.abs_nat (z - Fexp p)))%Z * powerRZ radix (Fexp p))%R in |- *. apply Rmult_lt_compat_r; auto with real zarith. now apply powerRZ_lt, IZR_lt. apply Rlt_le_trans with (IZR (Zpos (vNum b))). apply IZR_lt, H'. pattern (Zpos (vNum b)) at 1 in |- *; replace (Zpos (vNum b)) with (Zpos (vNum b) * 1)%Z; try ring. apply IZR_le, Zmult_le_compat_l. apply Zpower_NR1; lia. auto with zarith. rewrite inj_abs; auto with zarith; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz