proposition: Lemma wH_phase_shift (v : 'rV[F]_n) (m : nat) : wH (phase_shift v m.+1) = wH v.
proof: Proof. elim: m => [|m IH]. rewrite /phase_shift /wH !count_map. apply eq_count => i /=. by rewrite mxE mul1n mulf_eq0 negb_or expf_neq0 // andbT. rewrite -IH /phase_shift /wH !count_map. apply eq_count => i /=. by rewrite !mxE !mulf_eq0 !negb_or !expf_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming