proposition: Lemma pred_FLT_eq_FLX_large : forall beta emin prec, Prec_gt_0 prec -> forall x, bpow beta (emin + prec - 1) < x -> pred beta (FLT_exp emin prec) x = pred beta (FLX_exp prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x Hx. unfold pred, succ, pred_pos. destruct (Rle_bool_spec 0 (- x)) as [H | _]. { generalize (bpow_gt_0 beta (emin + prec - 1)). lra. } rewrite 3Ropp_involutive. revert Hx. destruct (Req_bool_spec x (bpow beta (mag beta x - 1))) as [-> | _]; intros Hx. { apply lt_bpow in Hx. rewrite mag_bpow. now rewrite <- FLX_FLT_aux by lia. } rewrite <-ulp_FLX_eq_FLT_large; [easy.. |]. left. apply Rlt_le_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