proposition: Lemma ulp_FLT_exact_shift : forall x e, (x <> 0)%R -> (emin + prec <= mag beta x)%Z -> (emin + prec - mag beta x <= e)%Z -> (ulp beta FLT_exp (x * bpow e) = ulp beta FLT_exp x * bpow e)%R.
proof: Proof. intros x e Nzx Hmx He. unfold ulp; rewrite Req_bool_false; [|now intro H; apply Nzx, (Rmult_eq_reg_r (bpow e)); [rewrite Rmult_0_l|apply Rgt_not_eq, Rlt_gt, bpow_gt_0]]. rewrite (Req_bool_false _ _ Nzx), <- bpow_plus; f_equal; unfold cexp, FLT_exp. rewrite (mag_mult_bpow _ _ _ Nzx), !Z.max_l; lia. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE