proposition: Lemma dimlen (k : nat) (C : t A B n [finType of 'rV[A]_k]) : 1 < #|A| -> k <= n.
proof: Proof. move=> F1. case : C => cws [] /= f. move/inj_card => /=. by rewrite !card_mx !mul1n leq_exp2l. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code