proposition: Theorem is_finite_strict_SF2B : forall x Hx, is_finite_strict (SF2B x Hx) = is_finite_strict_SF x.
proof: Proof. now intros [sx|sx| |sx mx ex] Hx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative