proposition: Lemma time_shift (an1 : a ^+ n = 1) (v : 'rV[F]_n) (m : nat) : dft (rVexp a n) n (phase_shift v m) = \row_i ((dft (rVexp a n) n v)``_(inord ((m + i) %% n))).
proof: Proof. apply/rowP => i. rewrite !mxE /fdcoor !horner_poly. apply/eq_bigr => /= j _. rewrite insubT // => jn. rewrite !mxE -mulrA (_ : Sub _ _ = j); last by apply val_inj. congr (_ * _). rewrite inordK ?ltn_pmod //. rewrite inordK //. rewrite inordK ?ltn_pmod //. move: (divn_eq (m + i) n); rewrite (addnC (_ %/ _ * _)%N). move/(congr1 (fun x => x - ((m + i) %/ n * n))%N); rewrite addnK => <-. rewrite -[in LHS]exprM -[in LHS]exprD. rewrite -[in RHS]exprM [in RHS]mulnBl. rewrite [in RHS]GRing.exprB; last 2 first. by rewrite leq_mul // leq_trunc_div. by rewrite unitfE. rewrite [in X in _ = _ / X]mulnAC [in X in _ = _ / X]mulnC. by rewrite [in X in _ = _ / X]exprM an1 expr1n divr1 mulnDl. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming