proposition: Lemma is_finite_Bone : is_finite Bone = true.
proof: Proof. unfold Bone. rewrite is_finite_BSN2B'. apply is_finite_Bone. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN