proposition: Lemma ulp_FLX_1 : ulp beta FLX_exp 1 = bpow (-prec + 1).
proof: Proof. unfold ulp, FLX_exp, cexp; rewrite Req_bool_false; [|apply R1_neq_R0]. rewrite mag_1; f_equal; ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE