proposition: Lemma ulp_FLX_le_FLT : forall (beta : radix) (emin prec : Z), Prec_gt_0 prec -> forall x : R, ulp beta (FLX_exp prec) x <= ulp beta (FLT_exp emin prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x. unfold ulp. destruct (Req_bool_spec x 0) as [-> | Hx]; [rewrite negligible_exp_FLX by easy |]. - destruct (negligible_exp_FLT emin prec) as [n [-> _]]. apply bpow_ge_0. - apply bpow_le. unfold cexp, FLX_exp, FLT_exp. lia. Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper