proposition: Lemma fdcoorB x y i : (x - y) ^`_ i = x ^`_ i - y ^`_ i.
proof: Proof. by rewrite /fdcoor linearB /= hornerD hornerN. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming