proposition: Lemma succ_FLT_exact_shift : forall x e, (x <> 0)%R -> (emin + prec + 1 <= mag beta x)%Z -> (emin + prec - mag beta x + 1 <= e)%Z -> (succ beta FLT_exp (x * bpow e) = succ beta FLT_exp x * bpow e)%R.
proof: Proof. intros x e Nzx Hmx He. destruct (Rle_or_lt 0 x) as [Px|Nx]. { now apply succ_FLT_exact_shift_pos; [lra|lia|lia]. } 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. { rewrite mag_opp; unfold FLT_exp; do 2 (rewrite Z.max_l; [|lia]). replace (_ - _)%Z with (mag beta x - 1 - prec + e)%Z; [|ring]. rewrite bpow_plus; ring. } rewrite ulp_FLT_exact_shift; [ring|lra| |]; rewrite mag_opp; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE