proposition: Theorem FPredDiff2 : forall x : float, Fnum x = nNormMin radix precision -> Fexp x = (- dExp b)%Z -> Fminus radix x (FPred x) = Float 1 (Fexp x) :>R.
proof: Proof. intros x H' H'0; rewrite (FPredFopFSucc x). pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x). rewrite <- Fopp_Fminus_dist. rewrite Fopp_Fminus. unfold FtoRradix in |- *; rewrite FSuccDiff2; auto. rewrite <- H'; case x; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz