proposition: Lemma num_occ_tuple_F2 a r (v : r.-tuple 'F_2): r./2 < N(a | v) -> N(negF2 a | v) <= N(a | v).
proof: Proof. move=> H. rewrite -(leq_add2l (N(a | v))) (num_occ_negF2 a v) addnn. rewrite (@leq_trans (r./2).*2.+1) // ?ltn_double //. rewrite -{1}(odd_double_half r) -addn1 addnC leq_add2l; by case: odd. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) hamming num_occ ssralg_ext f2 linearcode decoding channel_code