proposition: Lemma succ_round_FLX_le_FLT : forall beta emin prec, Prec_gt_0 prec -> forall rnd, Valid_rnd rnd -> forall x, generic_format beta (FLX_exp prec) x -> succ beta (FLX_exp prec) x <= succ beta (FLT_exp emin prec) (Generic_fmt.round beta (FLT_exp emin prec) rnd x).
proof: Proof. intros beta emin prec Iprec_gt_0 rnd Ivalid_rnd x Hx. generalize (FLX_exp_valid prec). intros Ivalid_exp_FLX. apply succ_le_lt; [easy.. | |]. - apply generic_format_FLX_FLT with emin. generalize (FLT_exp_valid emin prec). intros Ivalid_exp_FLT. apply generic_format_succ; [easy |]. now apply generic_format_round. - apply succ_round_gt_id; [now apply FLT_exp_valid | easy |]. unfold ulp. destruct (Req_bool_spec x 0) as [-> | Hxneq0]. + destruct (negligible_exp_FLT emin prec) as [n [-> _]]. generalize (bpow_gt_0 beta (FLT_exp emin prec n)). lra. + generalize (bpow_gt_0 beta (cexp beta (FLT_exp emin prec) x)). lra. 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