proposition: Theorem FF2B_B2FF_valid : forall x, FF2B (B2FF x) (valid_binary_B2FF x) = x.
proof: Proof. intros x. apply FF2B_B2FF. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN