proposition: Lemma round_FLX_mult_bpow: forall rnd, Valid_rnd rnd -> forall x e, round beta (FLX_exp prec) rnd (x*bpow e) = round beta (FLX_exp prec) rnd x*bpow e.
proof: Proof. Proof with auto with typeclass_instances. intros rnd Hrnd x e. case (Req_dec x 0); intros Hx. rewrite Hx, Rmult_0_l, round_0... ring. unfold round, FLX_exp, scaled_mantissa, cexp. rewrite mag_mult_bpow; try exact Hx. unfold F2R; simpl. rewrite Rmult_assoc; rewrite <- bpow_plus. rewrite Rmult_assoc; rewrite <- bpow_plus. f_equal; f_equal. f_equal; f_equal; f_equal; ring. ring. Qed.
imports: Coq(Reals Psatz) Flocq(Core) Interval(Tactic) ComputeMore Flocq(Bracket Round Operations Div)