proposition: Theorem is_nan_binary_normalize : forall mode m e szero, is_nan (binary_normalize mode m e szero) = false.
proof: Proof. intros mode m e szero. generalize (binary_normalize_correct mode m e szero). simpl. destruct Rlt_bool. - intros [_ [H _]]. now destruct binary_normalize. - intros H. rewrite <- is_nan_SF_B2SF. rewrite H. unfold binary_overflow. now destruct overflow_to_inf. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative