proposition: Lemma pred_FLT_exact_shift : forall x e, (x <> 0)%R -> (emin + prec + 1 <= mag beta x)%Z -> (emin + prec - mag beta x + 1 <= e)%Z -> (pred beta FLT_exp (x * bpow e) = pred beta FLT_exp x * bpow e)%R.
proof: Proof. intros x e Nzx Hmx He. unfold pred. rewrite Ropp_mult_distr_l. rewrite succ_FLT_exact_shift. apply Ropp_mult_distr_l. lra. now rewrite mag_opp. now rewrite mag_opp. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE