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