proposition: Lemma valid_binary_SF2FF : forall x, is_nan_SF x = false -> valid_binary (SF2FF x) = valid_binary_SF x.
proof: Proof. now intros [sx|sx| |sx mx ex] H. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN