proposition: Theorem FSuccSubnormal : forall a : float, Fsubnormal radix b a -> Fcanonic radix b (FSucc a).
proof: Proof. intros a H'. generalize (Z_eq_bool_correct (Fnum a) (Z.pred (nNormMin radix precision))); case (Z_eq_bool (Fnum a) (Z.pred (nNormMin radix precision))); intros H'1. left; apply FSuccSubnormNearNormMin; auto. right; apply FSuccSubnormNotNearNormMin; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz