数列の中間値定理１

　以前，HOL Light で書いた定理ですが，Isar では．．．

lemma
  fixes f :: "nat ⇒ real"
  assumes "f 0 < 0" "∃n. 0 ≦ f n"
  shows "∃n. f n < 0 ∧ 0 ≦ f (Suc n)"
proof (rule ccontr)
  assume 1: "¬ ?thesis"
  {fix n have "f n < 0"
    proof (induct n)
      show "f 0 < 0" by (fact assms)
      case (Suc n) then show ?case
      using 1 by auto
    qed
  } with assms show False by smt
qed