proposition: Theorem FSuccDiff3 : forall x : float, Fnum x = (- nNormMin radix precision)%Z -> Fexp x <> (- dExp b)%Z -> Fminus radix (FSucc x) x = Float 1 (Z.pred (Fexp x)) :>R.
proof: Proof. intros x H' H'1; rewrite FSuccSimpl2; auto. unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto. repeat rewrite Z.min_l; auto with zarith. rewrite <- Zminus_diag_reverse; rewrite Z.sub_pred_r; repeat rewrite <- Zminus_diag_reverse. rewrite absolu_Zs; auto with zarith; simpl in |- *. rewrite H'; unfold pPred in |- *; rewrite pGivesBound; unfold nNormMin in |- *. rewrite Z.opp_involutive; repeat rewrite Zmult_1_r. replace (Zpower_nat radix (pred precision) * radix)%Z with (Zpower_nat radix precision). unfold Z.pred in |- *; simpl in |- *; repeat rewrite plus_IZR || rewrite Ropp_Ropp_IZR. f_equal. simpl in |- *; ring. 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. Qed.
imports: Reals ZArith List PeanoNat Psatz