proposition: Lemma format_d_discri2 : format d.
proof: Proof. Proof with auto with typeclass_instances. unfold d; case (Rle_bool _ _). apply generic_format_round... apply generic_format_round... Qed.
imports: Psatz Core Plus_error Mult_error Operations Sterbenz Pff Pff2FlocqAux Nat2Z_compat