proposition: Lemma lel_Bit a b : (a <=l Bit b) = (a == Bit b).
proof: Proof. apply/idP/idP => [|/eqP ->]; last by rewrite lell. case/letterP : a b => //; by case/F2P. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode