proposition: Lemma U3_discri1 : b * b <> 0 -> a * c <> 0 -> p - q <> 0 -> bpow (emin + 2*prec) <= Rabs (round_flt (p-q)).
proof: Proof. Proof with auto with typeclass_instances. intros Z1 Z2 Z3. unfold Rminus; apply round_FLT_plus_ge... apply generic_format_round... apply generic_format_opp, generic_format_round... apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (2:=U1 Z1); apply bpow_le; lia. apply round_plus_neq_0... apply generic_format_round... apply generic_format_opp, generic_format_round... Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat