[STATEMENT]
lemma loc_upb_lm_2: "(c_fst n) mod 7 > 1 \<Longrightarrow> c_snd n < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
assume A1: "c_fst n mod 7 > 1"
[PROOF STATE]
proof (state)
this:
1 < c_fst n mod 7

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
1 < c_fst n mod 7
[PROOF STEP]
have S1: "1 < c_fst n"
[PROOF STATE]
proof (prove)
using this:
1 < c_fst n mod 7

goal (1 subgoal):
 1. 1 < c_fst n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < c_fst n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
have S2: "c_fst n \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_fst n \<le> n
[PROOF STEP]
by (rule c_fst_le_arg)
[PROOF STATE]
proof (state)
this:
c_fst n \<le> n

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S1 S2
[PROOF STATE]
proof (chain)
picking this:
1 < c_fst n
c_fst n \<le> n
[PROOF STEP]
have S3: "1 < n"
[PROOF STATE]
proof (prove)
using this:
1 < c_fst n
c_fst n \<le> n

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

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S3
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have S4: "n>1"
[PROOF STATE]
proof (prove)
using this:
1 < n

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

goal (1 subgoal):
 1. 1 < c_fst n mod 7 \<Longrightarrow> c_snd n < n
[PROOF STEP]
from S4
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. c_snd n < n
[PROOF STEP]
by (rule c_snd_less_arg)
[PROOF STATE]
proof (state)
this:
c_snd n < n

goal:
No subgoals!
[PROOF STEP]
qed