fact: Definition sum_letter (t : seq letter) := \sum_(l <- t) F2_of_letter l.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode