proposition: Theorem ulp_le : forall { Hm : Monotone_exp fexp }, forall x y: R, (Rabs x <= Rabs y)%R -> (ulp x <= ulp y)%R.
proof: Proof. intros Hm x y Hxy. rewrite <- ulp_abs. rewrite <- (ulp_abs y). apply ulp_le_pos; trivial. apply Rabs_pos. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop