proposition: Lemma Prod_cons_Star s : Prod (Star :: s) = Prod s.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode