[STATEMENT]
lemma seq_suble:
  assumes sf: "strict_mono (f :: nat \<Rightarrow> nat)"
  shows "n \<le> f n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<le> f n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> f 0
 2. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. 0 \<le> f 0
 2. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> f 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> f 0

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n \<le> f n

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
with sf [unfolded strict_mono_Suc_iff, rule_format, of n]
[PROOF STATE]
proof (chain)
picking this:
f n < f (Suc n)
n \<le> f n
[PROOF STEP]
have "n < f (Suc n)"
[PROOF STATE]
proof (prove)
using this:
f n < f (Suc n)
n \<le> f n

goal (1 subgoal):
 1. n < f (Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
n < f (Suc n)

goal (1 subgoal):
 1. \<And>n. n \<le> f n \<Longrightarrow> Suc n \<le> f (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < f (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n < f (Suc n)

goal (1 subgoal):
 1. Suc n \<le> f (Suc n)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
Suc n \<le> f (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed