proposition: Lemma succ_FLT_exact_shift_pos : forall x e, (0 < x)%R -> (emin + prec <= mag beta x)%Z -> (emin + prec - mag beta x <= e)%Z -> (succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.
proof: Proof. intros x e Px Hmx He. rewrite succ_eq_pos; [|now apply Rlt_le, Rmult_lt_0_compat, bpow_gt_0]. rewrite (succ_eq_pos _ _ _ (Rlt_le _ _ Px)). now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLT_exact_shift; [lra| |]. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE