proposition: Theorem mult_error_FLT_ge_bpow : forall x y e, format x -> format y -> (bpow (e+2*prec-1) <= Rabs (x * y))%R -> (round beta (FLT_exp emin prec) rnd (x * y) - (x * y) <> 0)%R -> (bpow e <= Rabs (round beta (FLT_exp emin prec) rnd (x * y) - (x * y)))%R.
proof: Proof. Proof with auto with typeclass_instances. intros x y e. set (f := (round beta (FLT_exp emin prec) rnd (x * y))). intros Fx Fy H1. unfold f; rewrite Fx, Fy, <- F2R_mult. simpl Fmult. destruct (round_repr_same_exp beta (FLT_exp emin prec) rnd (Ztrunc (scaled_mantissa beta (FLT_exp emin prec) x) * Ztrunc (scaled_mantissa beta (FLT_exp emin prec) y)) (cexp x + cexp y)) as (n,Hn). rewrite Hn; clear Hn. rewrite <- F2R_minus, Fminus_same_exp. intros K. eapply Rle_trans with (2:=F2R_ge _ K). simpl (Fexp _). apply bpow_le. unfold cexp, FLT_exp. destruct (mag beta x) as (ex,Hx). destruct (mag beta y) as (ey,Hy). simpl; apply Z.le_trans with ((ex-prec)+(ey-prec))%Z. 2: apply Zplus_le_compat; apply Z.le_max_l. cut (e + 2*prec -1< ex+ey)%Z. lia. apply lt_bpow with beta. apply Rle_lt_trans with (1:=H1). rewrite Rabs_mult, bpow_plus. apply Rmult_lt_compat. apply Rabs_pos. apply Rabs_pos. apply Hx. intros K'; contradict H1; apply Rlt_not_le. rewrite K', Rmult_0_l, Rabs_R0; apply bpow_gt_0. apply Hy. intros K'; contradict H1; apply Rlt_not_le. rewrite K', Rmult_0_r, Rabs_R0; apply bpow_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Core Operations Plus_error