proposition: Theorem FPredSimpl1 : forall x : float, Fnum x = (- pPred (vNum b))%Z -> FPred x = Float (- nNormMin radix precision) (Z.succ (Fexp x)).
proof: Proof. intros x H'; unfold FPred in |- *. generalize (Z_eq_bool_correct (Fnum x) (- pPred (vNum b))); case (Z_eq_bool (Fnum x) (- pPred (vNum b))); auto. intros H'0; contradict H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz