[STATEMENT]
lemma multiple_t_wise_balance: 
  assumes "n > 0" 
  shows "t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
interpret des: proper_design \<V> "(multiple_blocks n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_design \<V> (multiple_blocks n)
[PROOF STEP]
by (simp add: assms multiple_proper_design)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
using t_non_zero t_lt_order multiple_t_wise_balance_index
[PROOF STATE]
proof (prove)
using this:
1 \<le> \<t>
\<t> \<le> des.\<v>
\<lbrakk>?ps \<subseteq> \<V>; card ?ps = \<t>\<rbrakk> \<Longrightarrow> multiple_blocks ?n index ?ps = \<Lambda>\<^sub>t * ?n

goal (1 subgoal):
 1. t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)
[PROOF STEP]
by (unfold_locales) (simp_all)
[PROOF STATE]
proof (state)
this:
t_wise_balance \<V> (multiple_blocks n) \<t> (\<Lambda>\<^sub>t * n)

goal:
No subgoals!
[PROOF STEP]
qed