proposition: Theorem Fulp_zero : forall x : float, is_Fzero x -> Fulp x = powerRZ radix (- dExp b).
proof: Proof. intros x; unfold is_Fzero, Fulp, Fnormalize in |- *; case (Z_zerop (Fnum x)); simpl in |- *; auto. intros H' H'0; contradict H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz