proposition: Lemma B2BSN_lift : forall x y Ny, B2BSN (lift x y Ny) = y.
proof: Proof. intros x y Ny. unfold lift. destruct x as [sx|sx|sx px Px|sx mx ex Bx] ; simpl ; try apply B2BSN_BSN2B'. now destruct y. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN