proposition: Theorem FSuccDiff2 : forall x : float, Fnum x = (- nNormMin radix precision)%Z -> Fexp x = (- dExp b)%Z -> Fminus radix (FSucc x) x = Float 1 (Fexp x) :>R.
proof: Proof. intros x H' H'0; replace x with (Float (Fnum x) (Fexp x)). rewrite H'; rewrite H'0; rewrite FSuccSimpl3; auto. unfold FtoRradix, FtoR, Fminus, Fopp, Fplus in |- *; simpl in |- *; auto. repeat rewrite Zmin_n_n; repeat rewrite <- Zminus_diag_reverse; auto with zarith. simpl in |- *; repeat rewrite Zmult_1_r. rewrite Zplus_succ_l; rewrite Zplus_opp_r; simpl in |- *; auto. case x; simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz