proposition: Theorem round_FLT_FLX : forall rnd x, (bpow (emin + prec - 1) <= Rabs x)%R -> round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
proof: Proof. intros rnd x Hx. unfold round, scaled_mantissa. rewrite cexp_FLT_FLX ; trivial. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE