proposition: Lemma fdcoor_rcs (i : 'I_n) x : a ^+ n = 1 -> x ^`_ i = 0 -> (rcs x) ^`_ i = 0.
proof: Proof. move=> H1 H2; by rewrite (fdcoor_rcs' H1) // H2 mulr0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly polydiv vector) ssralg_ext poly_ext f2 hamming linearcode dft