proposition: Theorem mult_error_FLX : forall x y, format x -> format y -> format (round beta (FLX_exp prec) rnd (x * y) - (x * y))%R.
proof: Proof. intros x y Hx Hy. destruct (Req_dec (round beta (FLX_exp prec) rnd (x * y) - x * y) 0) as [Hr0|Hr0]. rewrite Hr0. apply generic_format_0. destruct (mult_error_FLX_aux x y Hx Hy Hr0) as ((m,e),(H1,(H2,H3))). rewrite <- H1. now apply generic_format_F2R. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error