proposition: Lemma idsA_ids1 (i : 'I_(n - m)) (j : 'I_m) : idsA `_ i <> sval (ids1 j).
proof: Proof. destruct (ids1 j) => /= Hij. have Hlti : i < size idsA by rewrite size_idsA. move: (mem_nth 0 Hlti). rewrite Hij => Hi. move: (imset_f (fun i => col i (Hamming.PCM m)) Hi). rewrite /idsA e. case/imsetP => y Hy Hy'. rewrite mem_filter -Hy' in Hy. move: (f_equal (fun c => wH c^T) Hy'). case Hj : (col j 1 \in non_unit_cols). by rewrite /non_unit_cols inE wH_col_1 in Hj. by rewrite Hj in Hy. 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