proposition: Lemma succ_FLX_exact_shift : forall x e, (succ beta FLX_exp (x * bpow e) = succ beta FLX_exp x * bpow e)%R.
proof: Proof. intros x e. destruct (Rle_or_lt 0 x) as [Px|Nx]. { rewrite succ_eq_pos; [|now apply Rmult_le_pos, bpow_ge_0]. rewrite (succ_eq_pos _ _ _ Px). now rewrite Rmult_plus_distr_r; f_equal; apply ulp_FLX_exact_shift. } unfold succ. rewrite Rle_bool_false; [|assert (H := bpow_gt_0 beta e); nra]. rewrite Rle_bool_false; [|now simpl]. rewrite Ropp_mult_distr_l_reverse, <-Ropp_mult_distr_l_reverse; f_equal. unfold pred_pos. rewrite mag_mult_bpow; [|lra]. replace (_ - 1)%Z with (mag beta (- x) - 1 + e)%Z; [|ring]; rewrite bpow_plus. unfold Req_bool; rewrite Rcompare_mult_r; [|now apply bpow_gt_0]. fold (Req_bool (-x) (bpow (mag beta (-x) - 1))); case Req_bool. { unfold FLX_exp. replace (_ - _)%Z with (mag beta (- x) - 1 - prec + e)%Z; [|ring]. rewrite bpow_plus; ring. } rewrite ulp_FLX_exact_shift; ring. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE