proposition: Lemma is_finite_B2BSN : forall x, BinarySingleNaN.is_finite (B2BSN x) = is_finite x.
proof: Proof. intros x. now destruct x. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN