proposition: Lemma num_occ_negF2 a r (v : r.-tuple 'F_2) : N(a | v) + N(negF2 a | v) = r.
proof: Proof. rewrite /num_occ -[RHS](size_tuple v) -[RHS](count_predC (fun x => a == x) v). congr (_ + _). apply eq_count => /= i; by rewrite inE eq_sym. apply eq_count => /= i; rewrite !inE. by case/F2P : i; case/F2P : a. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code