proposition: Theorem FSuccUlpPos : forall x : float, Fcanonic radix b x -> (0 <= x)%R -> Fminus radix (FSucc b radix precision x) x = Fulp x :>R.
proof: Proof. intros x H H0; rewrite CanonicFulp; auto. apply FSuccDiffPos; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz