proposition: Lemma err_mult_: forall x1 y1 e1 x2 y2 e2, format x1 -> format x2 -> err x1 y1 e1 -> err x2 y2 e2 -> (bpow (emin+prec-1) < Rabs (round_flt (x1*x2))) -> err (round_flt (x1*x2)) (y1*y2) (eps+(1+eps)*(e1+e2+e1*e2)).
proof: Proof. intros. case (err_mult_aux x1 y1 e1 x2 y2 e2); try assumption. easy. intros Y; contradict Y. now apply Rlt_not_le. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)