[STATEMENT]
lemma index_1_imp_mult_1: 
  assumes "\<Lambda> = 1"
  assumes "bl \<in># \<B>"
  assumes "card bl \<ge> 2"
  shows "multiplicity bl = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity bl = 1
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (multiplicity bl = 1)"
[PROOF STATE]
proof (state)
this:
multiplicity bl \<noteq> 1

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multiplicity bl \<noteq> 1
[PROOF STEP]
have "multiplicity bl \<noteq> 1" and "multiplicity bl \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 &&& multiplicity bl \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1
\<Lambda> = 1
bl \<in># \<B>
2 \<le> card bl

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 &&& multiplicity bl \<noteq> 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0
[PROOF STEP]
have m: "multiplicity bl \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
multiplicity bl \<noteq> 1
multiplicity bl \<noteq> 0

goal (1 subgoal):
 1. 2 \<le> multiplicity bl
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 \<le> multiplicity bl

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
obtain ps where ps: "ps \<subseteq> bl \<and> card ps = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps. ps \<subseteq> bl \<and> card ps = 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using nat_int_comparison(3) obtain_subset_with_card_n
[PROOF STATE]
proof (prove)
using this:
(?a \<le> ?b) = (int ?a \<le> int ?b)
\<lbrakk>?n \<le> card ?S; \<And>T. \<lbrakk>T \<subseteq> ?S; card T = ?n; finite T\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ps. ps \<subseteq> bl \<and> card ps = 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms(3))
[PROOF STATE]
proof (state)
this:
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ps \<subseteq> bl \<and> card ps = 2
[PROOF STEP]
have "\<B> index ps \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. 2 \<le> \<B> index ps
[PROOF STEP]
using m points_index_count_min ps
[PROOF STATE]
proof (prove)
using this:
ps \<subseteq> bl \<and> card ps = 2
2 \<le> multiplicity bl
\<lbrakk>?n \<le> multiplicity ?bl; ?ps \<subseteq> ?bl\<rbrakk> \<Longrightarrow> ?n \<le> \<B> index ?ps
ps \<subseteq> bl \<and> card ps = 2

goal (1 subgoal):
 1. 2 \<le> \<B> index ps
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2 \<le> \<B> index ps

goal (1 subgoal):
 1. multiplicity bl \<noteq> 1 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> \<B> index ps
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
2 \<le> \<B> index ps

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms index_distinct ps antisym_conv2 not_numeral_less_zero 
      numeral_le_one_iff points_index_ps_nin semiring_norm(69) zero_neq_numeral
[PROOF STATE]
proof (prove)
using this:
2 \<le> \<B> index ps
\<Lambda> = 1
bl \<in># \<B>
2 \<le> card bl
\<lbrakk>?G1.0 \<in> \<G>; ?G2.0 \<in> \<G>; ?G1.0 \<noteq> ?G2.0; ?x \<in> ?G1.0; ?y \<in> ?G2.0\<rbrakk> \<Longrightarrow> int (\<B> index {?x, ?y}) = \<Lambda>
ps \<subseteq> bl \<and> card ps = 2
?x \<le> ?y \<Longrightarrow> (\<not> ?x < ?y) = (?x = ?y)
\<not> numeral ?n < (0::?'a)
(numeral ?n \<le> (1::?'a)) = (?n \<le> num.One)
\<not> ?ps \<subseteq> \<V> \<Longrightarrow> \<B> index ?ps = 0
(num.Bit0 ?m \<le> num.One) = False
(0::?'a) \<noteq> numeral ?n

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis gdd_index_options int_int_eq int_ops(2))
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed