proposition: Lemma ulp_FLX_exact_shift : forall x e, (ulp beta FLX_exp (x * bpow e) = ulp beta FLX_exp x * bpow e)%R.
proof: Proof. intros x e. destruct (Req_dec x 0) as [Hx|Hx]. { unfold ulp. now rewrite !Req_bool_true, negligible_exp_FLX; rewrite ?Hx, ?Rmult_0_l. } unfold ulp; rewrite Req_bool_false; [|now intro H; apply Hx, (Rmult_eq_reg_r (bpow e)); [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]]. rewrite (Req_bool_false _ _ Hx), <- bpow_plus; f_equal; unfold cexp, FLX_exp. now rewrite mag_mult_bpow; [ring|]. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE