proposition: Lemma ulp_le_pos : forall { Hm : Monotone_exp fexp }, forall x y: R, (0 <= x)%R -> (x <= y)%R -> (ulp x <= ulp y)%R.
proof: Proof. Proof with auto with typeclass_instances. intros Hm x y Hx Hxy. destruct Hx as [Hx|Hx]. rewrite ulp_neq_0. rewrite ulp_neq_0. apply bpow_le. apply Hm. now apply mag_le. apply Rgt_not_eq, Rlt_gt. now apply Rlt_le_trans with (1:=Hx). now apply Rgt_not_eq. rewrite <- Hx. apply ulp_ge_ulp_0. apply monotone_exp_not_FTZ... Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop