proposition: Lemma ulp_FLX_eq_FLT_large : forall (beta : radix) (emin prec : Z), Prec_gt_0 prec -> forall x : R, bpow beta (emin + prec - 1) <= Rabs x -> ulp beta (FLX_exp prec) x = ulp beta (FLT_exp emin prec) x.
proof: Proof. intros beta emin prec Iprec_gt_0 x Hx. rewrite <-(ulp_abs _ (FLX_exp _)), <-(ulp_abs _ (FLT_exp _ _)). unfold ulp. destruct (Req_bool_spec (Rabs x) 0) as [H | _]; [generalize (bpow_gt_0 beta (emin + prec - 1)); lra |]. f_equal. unfold cexp. rewrite <-Rabs_Rabsolu in Hx. apply mag_gt_bpow in Hx. unfold 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