proposition: Theorem generic_format_B2R : forall x, generic_format radix2 fexp (B2R x).
proof: Proof. intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0. simpl. apply generic_format_canonical. now apply canonical_bounded. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative