proposition: Theorem FSuccSimpl2 : forall x : float, Fnum x = (- nNormMin radix precision)%Z -> Fexp x <> (- dExp b)%Z -> FSucc x = Float (- pPred (vNum b)) (Z.pred (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; absurd (0 <= pPred (vNum b))%Z; auto with zarith arith. rewrite <- H'1; rewrite H'. unfold nNormMin in |- *; simpl in |- *; auto with zarith. replace 0%Z with (- (0))%Z; auto with zarith. now apply Zlt_not_le, Zlt_Zopp, Zpower_nat_less. unfold pPred in |- *; apply Zle_Zpred; auto with zarith. intros H'1; generalize (Z_eq_bool_correct (Fnum x) (- nNormMin radix precision)); case (Z_eq_bool (Fnum x) (- nNormMin radix precision)). intros H'2; generalize (Z_eq_bool_correct (Fexp x) (- dExp b)); case (Z_eq_bool (Fexp x) (- dExp b)); auto. intros H'3; contradict H'0; auto. intros H'2; contradict H'2; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz