proposition: Lemma SF2FF_FF2SF : forall x, is_nan_FF x = false -> SF2FF (FF2SF x) = x.
proof: Proof. now intros [s|s|s m|s m e] H. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN