proposition: Lemma is_finite_SF2FF : forall x, is_finite_FF (SF2FF x) = is_finite_SF x.
proof: Proof. now intros [| | |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN