proposition: Theorem FSuccSimpl4 : forall x : float, Fnum x <> pPred (vNum b) -> Fnum x <> (- nNormMin radix precision)%Z -> FSucc x = Float (Z.succ (Fnum x)) (Fexp x).
proof: Proof. intros x H' H'0; 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'1; contradict H'; auto. intros H'1; generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision)); case (Z_eq_bool (Fnum x) (- nNormMin radix precision)); auto. intros H'2; contradict H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz