proposition: Theorem FPredSimpl2 : forall x : float, Fnum x = nNormMin radix precision -> Fexp x <> (- dExp b)%Z -> FPred x = Float (pPred (vNum b)) (Z.pred (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; absurd (0 < Fnum x)%Z; auto with zarith arith. apply Zle_not_lt; rewrite H'1; change 0%Z with (- (0))%Z; apply Zle_Zopp. unfold pPred in |- *; apply Zle_Zpred; red in |- *; simpl in |- *; auto. rewrite H'. apply nNormPos; 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