proposition: Lemma relative_error_FLT_aux : forall k, (emin + prec - 1 < k)%Z -> (prec <= k - FLT_exp emin prec k)%Z.
proof: Proof. intros k Hk. unfold FLT_exp. generalize (Zmax_spec (k - prec) emin). lia. Qed.
imports: Coq(ZArith Reals Psatz) Core