proposition: Theorem FSuccDiff1 : forall x : float, Fnum x <> (- nNormMin radix precision)%Z -> Fminus radix (FSucc x) x = Float 1 (Fexp x) :>R.
proof: Proof. intros x H'. generalize (Z_eq_bool_correct (Fnum x) (pPred (vNum b))); case (Z_eq_bool (Fnum x) (pPred (vNum b))); intros H'1. rewrite FSuccSimpl1; auto. unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto. repeat rewrite Z.min_r; auto with zarith. rewrite <- Zminus_succ_l; repeat rewrite <- Zminus_diag_reverse. rewrite absolu_Zs; auto with zarith; simpl in |- *. rewrite H'1; unfold pPred in |- *; rewrite pGivesBound; unfold nNormMin in |- *. replace (Zpower_nat radix (pred precision) * (radix * 1))%Z with (Zpower_nat radix precision). f_equal. unfold Z.pred. rewrite Z.opp_add_distr. rewrite Z.mul_1_r. rewrite Z.add_assoc. now rewrite Z.add_opp_diag_r. rewrite Z.mul_1_r. pattern precision at 1 in |- *; replace precision with (pred precision + 1). rewrite Zpower_nat_is_exp; rewrite Zpower_nat_1; auto. generalize precisionNotZero; case precision; simpl in |- *; auto with zarith arith. rewrite FSuccSimpl4; auto. unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; simpl in |- *. repeat rewrite Zmult_1_r. replace (Z.succ (Fnum x) + - Fnum x)%Z with (Z_of_nat 1). simpl in |- *; auto. simpl in |- *; unfold Z.succ in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz