proposition: Theorem FPredFopFSucc : forall x : float, FPred x = Fopp (FSucc b radix precision (Fopp x)).
proof: Proof. intros x. generalize (Z_eq_bool_correct (Fnum x) (- pPred (vNum b))); case (Z_eq_bool (Fnum x) (- pPred (vNum b))); intros H'1. rewrite FPredSimpl1; auto; rewrite FSuccSimpl1; auto. unfold Fopp in |- *; simpl in |- *; rewrite H'1; auto with zarith. 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)); intros H'3. replace x with (Float (Fnum x) (Fexp x)). rewrite H'2; rewrite H'3; rewrite FPredSimpl3; unfold Fopp in |- *; simpl in |- *; rewrite FSuccSimpl3; simpl in |- *; auto. rewrite <- Zopp_Zpred_Zs; rewrite Z.opp_involutive; auto. case x; simpl in |- *; auto. rewrite FPredSimpl2; auto; rewrite FSuccSimpl2; unfold Fopp in |- *; simpl in |- *; try rewrite Z.opp_involutive; auto. rewrite H'2; auto. rewrite FPredSimpl4; auto; rewrite FSuccSimpl4; auto. unfold Fopp in |- *; simpl in |- *; rewrite <- Zopp_Zpred_Zs; rewrite Z.opp_involutive; auto. unfold Fopp in |- *; simpl in |- *; contradict H'1; rewrite <- H'1; rewrite Z.opp_involutive; auto. unfold Fopp in |- *; simpl in |- *; contradict H'2; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz