proposition: Theorem FNPredFopFNSucc : forall x : float, FNPred x = Fopp (FNSucc b radix precision (Fopp x)).
proof: Proof. intros x; unfold FNPred, FNSucc in |- *; auto. rewrite Fnormalize_Fopp; auto. apply FPredFopFSucc; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz