proposition: Lemma fdcoor_loop_rcs k (i : 'I_n) (x : 'rV_n) : a ^+ n = 1 -> x ^`_ i = 0 -> (loop (@rcs F n) k x) ^`_ i = 0.
proof: Proof. move: i x. elim: k => // k IH i x an1 H /=. by rewrite IH // fdcoor_rcs. 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