proposition: Lemma PCM_A_1 : PCM = castmx (erefl, subnK (Hamming.dim_len m')) (row_mx CSM 1).
proof: Proof. apply/matrixP => i j. rewrite mxE castmxE /=. case/boolP : (j < n - m) => Hcond. have -> : cast_ord (esym (subnK (Hamming.dim_len m'))) j = lshift m (Ordinal Hcond) by apply val_inj. rewrite row_mxEl [in X in _ = X]mxE. rewrite castmxE /=. rewrite /PCM 2!cast_ord_id. rewrite esymK [in X in _ = X]mxE. by congr (Hamming.PCM m _ (systematic _)); exact: val_inj. rewrite [in X in _ = X]mxE. move: (splitP (cast_ord (esym (subnK (Hamming.dim_len m'))) j)) => [k Hk|k Hk]. have jk : j = k :> nat by []. by rewrite jk (ltn_ord k) in Hcond. rewrite permE /perm_ids. move Hj : (ord_split j) => l. move: (splitP l) => [p Hp|p Hlp]. exfalso. move/negP : Hcond; apply. suff -> : nat_of_ord j = nat_of_ord p by apply ltn_ord. by rewrite -Hp -Hj. destruct ids1 as [x e] => /=. move/matrixP/(_ i 0) : e. rewrite !mxE => -> /=. rewrite cast_ord_id; congr (_ == _)%:R. apply/val_inj/eqP => /=. by rewrite -(eqn_add2l (n - m)) -Hlp -Hj Hk. 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