proposition: Theorem FPredDiff1 : forall x : float, Fnum x <> nNormMin radix precision -> Fminus radix x (FPred x) = Float 1 (Fexp x) :>R.
proof: Proof. intros x H'; rewrite (FPredFopFSucc x). pattern x at 1 in |- *; rewrite <- (Fopp_Fopp x). rewrite <- Fopp_Fminus_dist. rewrite Fopp_Fminus. unfold FtoRradix in |- *; rewrite FSuccDiff1; auto. replace (Fnum (Fopp x)) with (- Fnum x)%Z. contradict H'; rewrite <- (Z.opp_involutive (Fnum x)); rewrite H'; auto with zarith. case x; simpl in |- *; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz