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