[STATEMENT]
theorem FNTT_correct:
  assumes "length numbers = n"
  shows "FNTT numbers = NTT numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT numbers = NTT numbers
[PROOF STEP]
using FNTT_NTT_gen_eq NTT_gen_NTT_full_length assms n_two_pot
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?numbers = 2 ^ ?l; 2 ^ ?l \<le> n\<rbrakk> \<Longrightarrow> FNTT ?numbers = NTT_gen (length ?numbers) ?numbers
length ?numbers = n \<Longrightarrow> NTT_gen n ?numbers = NTT ?numbers
length numbers = n
n = 2 ^ N

goal (1 subgoal):
 1. FNTT numbers = NTT numbers
[PROOF STEP]
by force