proposition: Theorem is_nan_Bulp : forall x, is_nan (Bulp x) = is_nan x.
proof: Proof. intros [sx|sx| |sx mx ex Bx] ; try easy. unfold Bulp. apply is_nan_binary_normalize. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative