proposition: Theorem ulp_canonical : forall m e, m <> 0%Z -> canonical beta fexp (Float beta m e) -> ulp (F2R (Float beta m e)) = bpow e.
proof: Proof. intros m e Hm Hc. rewrite ulp_neq_0 by now apply F2R_neq_0. apply f_equal. now apply sym_eq. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop