proposition: Theorem is_finite_strict_Bone : is_finite_strict Bone = true.
proof: Proof. apply is_finite_strict_B2R. rewrite Bone_correct. apply R1_neq_R0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative