proposition: Lemma ulp_ge_ulp_0 : Exp_not_FTZ fexp -> forall x, (ulp 0 <= ulp x)%R.
proof: Proof. unfold Exp_not_FTZ; intros H x. case (Req_dec x 0); intros Hx. rewrite Hx; now right. unfold ulp at 1. rewrite Req_bool_true; trivial. case negligible_exp_spec'. intros (H1,H2); rewrite H1; apply ulp_ge_0. intros (n,(H1,H2)); rewrite H1. rewrite ulp_neq_0; trivial. apply bpow_le; unfold cexp. generalize (mag beta x); intros l. case (Zle_or_lt l (fexp l)); intros Hl. rewrite (fexp_negligible_exp_eq n l); trivial; apply Z.le_refl. case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K. absurd (fexp n <= fexp l)%Z. lia. apply Z.le_trans with (2:= H _). apply Zeq_le, sym_eq, valid_exp; trivial. lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop