proposition: Lemma no_weight_2_cw x : wH x = 2%N -> syndrome H x <> 0.
proof: Proof. move=> /wH_2[i [j [Hij [Hi [Hj Hk]]]]]. rewrite /syndrome mulmx_sum_col (bigID (pred1 i)) /= big_pred1_eq /=. rewrite (bigID (pred1 j)) /= (eq_bigl (pred1 j)) /=; last first. move=> a /=; case/boolP : (a == j) => aj; last by rewrite andbC. rewrite andbC /= (eqP aj) eq_sym; by apply/eqP. rewrite big_pred1_eq /= (eq_bigr (fun=> 0)) /=; last first. move=> a /andP[X1 X2]. rewrite mxE Hk ?scale0r //; (apply/eqP; by rewrite eq_sym). rewrite big_const_seq /= iter_addr0_cV /= 2!mxE Hi Hj 2!scale1r addr0. rewrite linearD /= 2!col_matrix 2!trmxK. apply rV_of_natD_neq0 => //. - by apply/eqP; move/eqP : Hij; apply contra => /eqP[]/eqP. - by rewrite -(addn1 i) addnC -ltn_subRL subn1 -Hamming.len_dim. - by rewrite -(addn1 j) addnC -ltn_subRL subn1 -Hamming.len_dim. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel