proposition: Theorem FulpLe2 : forall p : float, Fbounded b p -> Fnormal radix b (Fnormalize radix b precision p) -> (Fulp p <= Rabs p * powerRZ radix (Z.succ (- precision)))%R.
proof: Proof. intros p H1 H2; unfold Fulp in |- *. replace (FtoRradix p) with (FtoRradix (Fnormalize radix b precision p)); [ idtac | unfold FtoRradix in |- *; apply FnormalizeCorrect; auto ]. apply Rmult_le_reg_l with (powerRZ radix (Z.pred precision)). apply powerRZ_lt, IZR_lt; auto with real arith. replace (powerRZ radix (Z.pred precision) * (Rabs (Fnormalize radix b precision p) * powerRZ radix (Z.succ (- precision))))%R with (Rabs (Fnormalize radix b precision p)). unfold FtoRradix in |- *; rewrite <- Fabs_correct; auto with arith real. unfold Fabs, FtoR in |- *; simpl in |- *. apply Rmult_le_compat_r; [ apply powerRZ_le, IZR_lt | rewrite <- inj_pred ]; auto with real arith zarith. rewrite <- Zpower_nat_Z_powerRZ. replace (Zpower_nat radix (pred precision)) with (nNormMin radix precision); auto; apply IZR_le. apply pNormal_absolu_min with b; auto with arith zarith real. apply trans_eq with (Rabs (Fnormalize radix b precision p) * (powerRZ radix (Z.pred precision) * powerRZ radix (Z.succ (- precision))))%R; [ idtac | ring ]. rewrite <- powerRZ_add; auto with zarith real. replace (Z.pred precision + Z.succ (- precision))%Z with 0%Z; [ simpl in |- *; ring | unfold Z.succ, Z.pred in |- *; ring ]; auto with real zarith. apply IZR_neq; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz