proposition: Lemma format_dp : format dp.
proof: Proof. Proof with auto with typeclass_instances. replace (dp) with (-(p-(b*b))) by (unfold dp; ring). apply generic_format_opp. apply mult_error_FLT... intros Zbb; apply Rle_trans with (2:=U1 Zbb). apply bpow_le; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat