proposition: Lemma no_weight_1_cw x : wH x = 1%N -> syndrome H x <> 0.
proof: Proof. move=> /wH_1[i [Hi Hi']]. rewrite /syndrome mulmx_sum_col (bigID (pred1 i)) /= big_pred1_eq /=. rewrite (eq_bigr (fun=> 0)) /=; last first. move=> j; rewrite eq_sym => /eqP/Hi'; rewrite mxE => ->; by rewrite scale0r. rewrite big_const_seq /= iter_addr0_cV mxE Hi scale1r addr0 col_matrix trmxK. apply rV_of_nat_neq0 => //. by rewrite -(addn1 i) 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