proposition: Theorem round_round_mult : forall (fexp1 fexp2 : Z -> Z), round_round_mult_hyp fexp1 fexp2 -> forall x y, generic_format beta fexp1 x -> generic_format beta fexp1 y -> round beta fexp1 rnd (round beta fexp2 rnd (x * y)) = round beta fexp1 rnd (x * y).
proof: Proof. intros fexp1 fexp2 Hfexp x y Fx Fy. assert (Hxy : round beta fexp2 rnd (x * y) = x * y). { apply round_generic; [assumption|]. now apply (round_round_mult_aux fexp1 fexp2). } now rewrite Hxy at 1. Qed.
imports: Coq(ZArith Reals Psatz) Core FTZ