proposition: Lemma pred_FLX_exact_shift : forall x e, (pred beta FLX_exp (x * bpow e) = pred beta FLX_exp x * bpow e)%R.
proof: Proof. intros x e. unfold pred. rewrite Ropp_mult_distr_l, succ_FLX_exact_shift. apply Ropp_mult_distr_l. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE