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