proposition: Theorem ulp_le_abs: forall x, (x <> 0)%R -> F x -> (ulp x <= Rabs x)%R.
proof: Proof. intros x Zx Fx. rewrite <- ulp_abs. apply ulp_le_id. now apply Rabs_pos_lt. now apply generic_format_abs. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop