proposition: Theorem is_finite_strict_B2R : forall x, B2R x <> 0%R -> is_finite_strict x = true.
proof: Proof. now intros [sx|sx| |sx mx ex Bx] Hx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative