proposition: Theorem FSuccSimpl1 : forall x : float, Fnum x = pPred (vNum b) -> FSucc x = Float (nNormMin radix precision) (Z.succ (Fexp x)).
proof: Proof. intros x H'; unfold FSucc 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