proposition: Lemma fdcoor0 i : (0 : 'rV_n) ^`_ i = 0.
proof: Proof. by rewrite /fdcoor linear0 horner0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming