proposition: Theorem valid_binary_B2FF : forall x, valid_binary (B2FF x) = true.
proof: Proof. now intros [sx|sx|sx plx Hplx|sx mx ex Hx]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN