proposition: Theorem FLT_format_B2R : forall x, FLT_format radix2 emin prec (B2R x).
proof: Proof. Proof with auto with typeclass_instances. intros x. apply FLT_format_generic... apply generic_format_B2R. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative