proposition: Lemma SF2R_FF2SF : forall beta x, SF2R beta (FF2SF x) = FF2R beta x.
proof: Proof. now intros beta [s|s|s m|s m e]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN