proposition: Lemma format_dq : format dq.
proof: Proof. Proof with auto with typeclass_instances. replace (dq) with (-(q-(a*c))) by (unfold dq; ring). apply generic_format_opp. apply mult_error_FLT... intros Zac; apply Rle_trans with (2:=U2 Zac). apply bpow_le; lia. Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat