proposition: Lemma U5_discri1 : b * b <> 0 -> a*c <> 0 -> round_flt (dp - dq) <> dp - dq -> bpow (emin + prec - 1) <= Rabs (round_flt (dp - dq)).
proof: Proof. Proof with auto with typeclass_instances. intros Z1 Z2 Z3. apply U5_discri1_aux. apply format_dp... apply generic_format_opp, format_dq... lia. unfold dp; replace (b * b - p) with (-(p-b*b)) by ring. rewrite Rabs_Ropp; unfold p. apply mult_error_FLT_ge_bpow... apply Rle_trans with (2:=U1 Z1). apply bpow_le; lia. replace (round_flt (b * b) - b * b) with (-dp). apply Ropp_neq_0_compat. intros Z4; contradict Z3. rewrite Z4, Rminus_0_l, round_generic... apply generic_format_opp, format_dq... unfold dp, p; ring. unfold dq; replace (-(a * c - q)) with (q-a*c) by ring. unfold q; apply mult_error_FLT_ge_bpow... apply Rle_trans with (2:=U2 Z2). apply bpow_le; lia. replace (round_flt (a * c) - a * c) with (-dq). apply Ropp_neq_0_compat. intros Z4; contradict Z3. rewrite Z4, Rminus_0_r, round_generic... apply format_dp... unfold dq, q; ring. easy. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat