[STATEMENT]
lemma INTT_gen_INTT_full_length:
  assumes "length numbers =n"
  shows "INTT_gen n numbers = INTT numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. INTT_gen n numbers = INTT numbers
[PROOF STEP]
unfolding INTT_gen_def intt_gen_def INTT_def intt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. \<Sum>j = 0..<length numbers. numbers ! j * \<mu> ^ (n div n * i * j)) [0..<length numbers] = map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<mu> ^ (i * j)) [0..<n]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length numbers = n

goal (1 subgoal):
 1. map (\<lambda>i. \<Sum>j = 0..<length numbers. numbers ! j * \<mu> ^ (n div n * i * j)) [0..<length numbers] = map (\<lambda>i. \<Sum>j = 0..<n. numbers ! j * \<mu> ^ (i * j)) [0..<n]
[PROOF STEP]
by simp


[STATEMENT]
lemma my_div_exp_min1:
  assumes "2^(Suc l) \<le> n"
  shows "(\<mu> ^(n div 2^(Suc l)))^(2^l) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> ^ (n div 2 ^ Suc l)) ^ 2 ^ l = - 1
[PROOF STEP]
by (metis assms divide_minus1 mult_zero_right mu_properties(1) nonzero_mult_div_cancel_right omega_div_exp_min1 power_one_over zero_neq_one)


[STATEMENT]
lemma my_n_2_min1:  "\<mu>^(n div 2) = -1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> ^ (n div 2) = - 1
[PROOF STEP]
by (metis divide_minus1 mult_zero_right mu_properties(1) nonzero_mult_div_cancel_right omg_n_2_min1 power_one_over zero_neq_one)