proposition: Lemma succ_FLX_eq_FLT_large : forall beta emin prec, Prec_gt_0 prec -> forall x, bpow beta (emin + prec - 1) <= x -> succ beta (FLX_exp prec) x = succ beta (FLT_exp emin prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x Hx. unfold succ, pred_pos. destruct (Rle_bool_spec 0 x) as [_ | H]. 2: generalize (bpow_gt_0 beta (emin + prec - 1)); lra. rewrite <-ulp_FLX_eq_FLT_large; [easy.. |]. apply Rle_trans with (1 := Hx), Rle_abs. 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