数列の中間値定理２

　いわゆる one line proof です．

lemma
  "(f::nat⇒real) 0 < 0 ==> ∃n. 0 ≦ f n ==> ∃n. f n < 0 ∧ 0 ≦ f (Suc n)"
by (metis nat_induct [of "%n. f n < 0"] not_le)

参照している定理は

thm nat_induct [of "%n. f n < 0"] not_le

f 0 < 0 ⟹ (⋀n. f n < 0 ⟹ f (Suc n) < 0) ⟹ f ?n < 0
(¬ ?x ≤ ?y) = (?y < ?x)

の２つですが，Z3 は not_le を知っているので

lemma
  "(f::nat⇒real) 0 < 0 ==> ∃n. 0 ≦ f n ==> ∃n. f n < 0 ∧ 0 ≦ f (Suc n)"
by (smt nat_induct [of "%n. f n < 0"])

とも出来ます．