proposition: Lemma letter_split (l : letter) : [exists b, l == Bit b] || (starblank l).
proof: Proof. case/letterP : l; rewrite ?orbT //. by apply/orP; left; apply/existsP; exists 0. by apply/orP; left; apply/existsP; exists 1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode