proposition: Theorem FNSuccCanonic : forall a : float, Fbounded b a -> Fcanonic radix b (FNSucc a).
proof: Proof. intros a H'; unfold FNSucc in |- *. apply FSuccCanonic; auto with zarith. apply FnormalizeCanonic; easy. Qed.
imports: Reals ZArith List PeanoNat Psatz