for n, ni being non zero Element of NAT
for q being Integer st ni < n & ni divides n holds
for qc being Element of F_Complex st qc = q holds
for j, k, l being Integer st j = eval ((cyclotomic_poly n),qc) & k = eval ((unital_poly (F_Complex,n)),qc) & l = eval ((unital_poly (F_Complex,ni)),qc) holds
j divides k div l