proposition: Lemma ulp_ulp_0 : forall {H : Exp_not_FTZ fexp}, ulp (ulp 0) = ulp 0.
proof: Proof. intros H; case (negligible_exp_spec'). intros (K1,K2). replace (ulp 0) with 0%R at 1; try easy. apply sym_eq; unfold ulp; rewrite Req_bool_true; try easy. now rewrite K1. intros (n,(Hn1,Hn2)). apply Rle_antisym. replace (ulp 0) with (bpow (fexp n)). rewrite ulp_bpow. apply bpow_le. now apply valid_exp. unfold ulp; rewrite Req_bool_true; try easy. rewrite Hn1; easy. now apply ulp_ge_ulp_0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop