proposition: Theorem ulp_FIX : forall x, ulp beta FIX_exp x = bpow emin.
proof: Proof. intros x; unfold ulp. case Req_bool_spec; intros Zx. case (negligible_exp_spec FIX_exp). intros T; specialize (T (emin-1)%Z); contradict T. unfold FIX_exp; lia. intros n _; reflexivity. reflexivity. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE