proposition: Theorem FNevenSuc : forall p : float, Fbounded b p -> FNeven p -> FNodd (FNSucc b radix precision p).
proof: Proof. unfold FNodd, FNeven, FNSucc in |- *. intros p H' H'0. rewrite FcanonicFnormalizeEq; auto with zarith arith. apply FevenSuc; auto. apply FSuccCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz