proposition: Lemma succ_FLX_le_FLT : forall beta emin prec, Prec_gt_0 prec -> forall x, succ beta (FLX_exp prec) x <= succ beta (FLT_exp emin prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x. unfold succ. case (Rle_bool 0 x); [now apply Rplus_le_compat_l, ulp_FLX_le_FLT |]. unfold pred_pos. case (Req_bool (- x) (bpow beta (mag beta (- x) - 1))); rewrite 2Ropp_minus_distr; apply Rplus_le_compat_r; [apply bpow_le; unfold FLT_exp, FLX_exp; lia | now apply ulp_FLX_le_FLT]. 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