proposition: Theorem FPredSimpl4 : forall x : float, Fnum x <> (- pPred (vNum b))%Z -> Fnum x <> nNormMin radix precision -> FPred x = Float (Z.pred (Fnum x)) (Fexp x).
proof: Proof. intros x H' H'0; 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'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