proposition: Fact ex1 x y : x <> 0 -> Monotone_exp phi -> Rabs x <= Rabs y -> ulp r phi x <= ulp r phi y.
proof: Proof. intros NZx Mphi Rxy. assert (NZy : y <> 0) by (split_Rabs; lra). rewrite !ulp_neq_0; auto. apply bpow_le. apply Mphi. apply mag_le_abs; assumption. Qed.
imports: Psatz ZArith Reals SpecFloat Flocq(FTZ Core Operations BinarySingleNaN Binary Bits)