[STATEMENT]
lemma nan_not_finite[simp]: "is_nan x \<Longrightarrow> \<not> is_finite x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nan x \<Longrightarrow> \<not> is_finite x
[PROOF STEP]
using float_distinct_finite(1)
[PROOF STATE]
proof (prove)
using this:
\<not> (is_nan ?a \<and> is_finite ?a)

goal (1 subgoal):
 1. is_nan x \<Longrightarrow> \<not> is_finite x
[PROOF STEP]
by blast