proposition: Theorem FIX_format_FLX : forall x e, (bpow (e - 1) <= Rabs x <= bpow e)%R -> FLX_format x -> FIX_format beta (e - prec) x.
proof: Proof. clear prec_gt_0_. intros x e Hx [[xm xe] H1 H2]. rewrite H1, (F2R_prec_normalize beta xm xe e prec). now eexists. exact H2. now rewrite <- H1. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE