proposition: Lemma dft_shifting (an1 : a ^+ n = 1) (v : 'rV[F]_n) m (mn : m < n) : (forall i : 'I_n, 0 < i < m.+1 -> (dft (rVexp a n) n v) ``_ i = 0) -> let w := phase_shift v m.+1 in (forall i : 'I_n, n - m <= i < n -> (dft (rVexp a n) n w) ``_ i = 0).
proof: Proof. move=> H w i Hi. rewrite time_shift // mxE H // inordK // ?ltn_pmod //. have /andP [Hi'1 Hi'2] : n < i + m.+1 < n + m.+1. case/andP : Hi => Hi1 Hi2. by rewrite ltn_add2r Hi2 andbT addnC -leq_subLR subSS. rewrite -(subn0 (m.+1 + i)%N). apply/andP. rewrite -{-1}(subnn n) subnBA // addnC -addnBA; last by rewrite addnC ltnW. rewrite modnDl modn_small; last first. rewrite addnC -(ltn_add2r n) subnK; last by rewrite ltnW. by rewrite (leq_trans Hi'2) // leq_add2l. split; first by rewrite subn_gt0 addnC. by rewrite -(ltn_add2r n) subnK ?ltn_add2l // addnC ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming