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