proposition: Lemma FLX_FLT_aux : forall (emin prec e : Z), (emin + prec - 1 < e)%Z -> FLX_exp prec e = FLT_exp emin prec e.
proof: Proof. 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