proposition: Lemma dH_num_occ_opp r a (v : 'rV_ r) : dH (const_mx a) v = N(negF2 a | tuple_of_row v).
proof: Proof. rewrite /dH /wH. rewrite (_ : tuple_of_row _ = [tuple of map (fun x => F2_of_bool (x != a%R)) (tuple_of_row v)]); last first. apply eq_from_tnth => i. rewrite tnth_mktuple tnth_map tnth_mktuple !mxE. by case/F2P : a; case: F2P => //; rewrite subrr. rewrite {1}/num_occ count_map /preim. apply eq_count => /= x. rewrite !inE. by case/F2P : a; case/F2P : x. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code