proposition: Theorem is_finite_FF2B : forall x Hx, is_finite (FF2B x Hx) = is_finite_FF x.
proof: Proof. now intros [| | |]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN