proposition: Lemma V2_Und5: a*x <> 0 -> r1 = 0 \/ bpow beta (emin + prec-1) <= Rabs r1.
proof: Proof. Proof with auto with typeclass_instances. intros Zax. case (Req_dec r1 0); intros Zr1. now left. case U1; intros H. now contradict H. right. case U2; intros Hy. unfold r1; rewrite Hy, Rplus_0_r. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=H). apply bpow_le; lia. unfold r1; replace (a*x)%R with (u1+u2)%R. 2: unfold u2, u1; ring. case (Req_dec u2 0); intros Zu2. rewrite Zu2, Rplus_0_r. case (Req_dec (round_flt (u1 + y)) 0%R); intros L. contradict Zr1. unfold r1; replace (a*x)%R with (u1+u2)%R. 2: unfold u2, u1; ring. now rewrite Zu2, Rplus_0_r. rewrite Rplus_comm; apply round_FLT_plus_ge... apply generic_format_round... apply Rle_trans with (2:=Hy). apply bpow_le; lia. now rewrite Rplus_comm. assert (T:round_flt (u1 + y) <> 0 -> (bpow beta (emin + 3 * prec - 2 - prec) <= Rabs (round_flt (u1 + y)))). intros K; apply round_FLT_plus_ge... apply generic_format_round... apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=H). apply bpow_le; lia. case (Req_dec (u1+y) 0); intros H1. replace (u1+u2+y) with (u1+y+u2) by ring. rewrite H1, Rplus_0_l. case (mult_error_FLT_ge_bpow' a x (emin + 4 * prec - 3)); try assumption. intros H2; contradict Zr1. unfold r1; replace (a*x)%R with (u1+u2)%R. 2: unfold u2, u1; ring. replace (u1+u2+y) with (u1+y+u2) by ring. rewrite H1, Rplus_0_l. unfold u2, u1; rewrite H2, round_0... fold u1 u2; intros H2. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=H2). apply bpow_le; lia. generalize Zr1; unfold r1. replace (a*x)%R with (u1+u2)%R. 2: unfold u2, u1; ring. replace (u1+u2+y) with ((u1+y)+u2) by ring. assert (Fu2: format u2). replace (u2) with (-(u1-(a*x))) by (unfold u2; ring). apply generic_format_opp. apply mult_error_FLT... intros L; case U1; intros J; try easy. apply Rle_trans with (2:=J); apply bpow_le. lia. intros K; apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. assert (K':u1 + y + u2 <> 0). intros L; apply K; rewrite L. apply round_0... generalize K'. unfold u1; unfold round. rewrite Fy, Fu2. rewrite <- F2R_plus, <- F2R_plus. intros L. apply Rle_trans with (2:=F2R_ge _ _ L). rewrite 2!Fexp_Fplus. apply bpow_le. apply Z.min_glb. apply Z.min_glb. simpl. apply Z.le_trans with (FLT_exp emin prec (emin +3*prec-1)). unfold FLT_exp. rewrite Z.max_l; lia. apply cexp_ge_bpow... apply Rle_trans with (2:=H). apply bpow_le; lia. simpl. apply Z.le_trans with (FLT_exp emin prec (emin +2*prec+1)). unfold FLT_exp. rewrite Z.max_l; lia. apply cexp_ge_bpow... apply Rle_trans with (2:=Hy). apply bpow_le; lia. simpl. apply Z.le_trans with (FLT_exp emin prec (emin +2*prec-1)). unfold FLT_exp. rewrite Z.max_l; lia. apply cexp_ge_bpow... case (mult_error_FLT_ge_bpow' a x (emin+4*prec-3)); try assumption. intros Z; contradict Zu2. unfold u2, u1; easy. intros H2. apply Rle_trans with (2:=H2). apply bpow_le. lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat