proposition: Lemma Bsign_B2BSN : forall x, is_nan x = false -> BinarySingleNaN.Bsign (B2BSN x) = Bsign x.
proof: Proof. now intros [s|s| |s m e H]. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN