proposition: Theorem ulp_abs : forall x, ulp (Rabs x) = ulp x.
proof: Proof. intros x. unfold ulp; case (Req_bool_spec x 0); intros H1. rewrite Req_bool_true; trivial. now rewrite H1, Rabs_R0. rewrite Req_bool_false. now rewrite cexp_abs. now apply Rabs_no_R0. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop