proposition: Lemma Prod_Bit (b : 'F_2) s : Prod s = Bit b -> Bit b \in s.
proof: Proof. rewrite /Prod. case: ifPn => [H [<-] | H]; first by rewrite mem_num_occ_gt0 (leq_trans _ H). case: ifPn => // H' [<-]; by rewrite mem_num_occ_gt0 (leq_trans _ H'). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode