proposition: Lemma mult_error_FLT_ge_bpow': forall a b e, format a -> format b -> a*b = 0 \/ bpow beta e <= Rabs (a*b) -> a*b-round_flt (a*b) = 0 \/ bpow beta (e+1-2*prec) <= Rabs (a*b-round_flt (a*b)).
proof: Proof. Proof with auto with typeclass_instances. intros a b e Fa Fb H. case (Req_dec (a * b - round_flt (a * b)) 0); intros Z1;[now left|right]. rewrite <- Rabs_Ropp. replace (- (a * b - round_flt (a * b))) with (round_flt (a * b) - a*b) by ring. case H; intros H'. contradict Z1. rewrite H', round_0... ring. apply mult_error_FLT_ge_bpow... apply Rle_trans with (2:=H'); apply bpow_le; lia. replace (round_flt (a * b) - a*b) with (- (a * b - round_flt (a * b))) by ring. now apply Ropp_neq_0_compat. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat