proposition: Lemma Sum_blank_inv s : Sum s != Blank.
proof: Proof. rewrite /Sum; by case: ifP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode