proposition: Theorem FF2B_B2FF : forall x H, FF2B (B2FF x) H = x.
proof: Proof. intros [sx|sx|sx plx Hplx|sx mx ex Hx] H ; try easy. apply f_equal, eqbool_irrelevance. apply f_equal, eqbool_irrelevance. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN