proposition: Lemma U4_discri1 : b * b <> 0 -> a * c <> 0 -> p - q <> 0 -> bpow (emin + prec) <= Rabs d.
proof: Proof. Proof with auto with typeclass_instances. intros Z1 Z2 Z3; generalize Zd; unfold d. case (Rle_bool_spec _ _); intros H Z4. apply Rle_trans with (2:=U3_discri1 Z1 Z2 Z3). apply bpow_le; lia. apply round_FLT_plus_ge... apply generic_format_round... apply generic_format_round... replace (emin + prec + prec)%Z with (emin+2*prec)%Z by ring. apply U3_discri1; easy. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat