proposition: Theorem FSuccPosNotMax : forall a : float, (0 <= a)%R -> Fcanonic radix b a -> Fcanonic radix b (FSucc a).
proof: Proof. intros a H' H'0; case H'0; intros H'2. left; apply FSuccNormPos; auto. apply FSuccSubnormal; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz