proposition: Lemma PCM_GEN'_alt : PCM *m GEN'^T = 0.
proof: Proof. have H1 : (n - m <= n)%nat by apply leq_subr. have H2 : (m = n - (n - m))%nat by rewrite (subnBA _ (Hamming.dim_len m')) addnC addnK. move: (Syslcode.H_G_T H1 (castmx (H2, erefl (n - m)%nat) CSM)) => /=. rewrite /Syslcode.PCM /= /Syslcode.GEN /= => H0. rewrite PCM_A_1 /GEN' !F2_mx_opp. apply/matrixP => a b. rewrite [in X in _ = X]mxE. move/matrixP : H0. move/(_ (cast_ord H2 a) b). rewrite [in X in _ = X -> _]mxE => <-. rewrite !mxE. apply eq_bigr; case=> i Hi _ /=. congr (_ * _). rewrite !castmxE /= !cast_ord_id !mxE. case: splitP. - case=> j Hj /= ?; subst j. case: splitP. + case=> j Hj_ /= ?; subst j. rewrite castmxE /= cast_ord_id. f_equal; by apply val_inj. + case=> k Hk /= ?; subst i. exfalso. by rewrite ltnNge leq_addr in Hj. - case=> k Hk /= ?; subst i. case: splitP. + case=> j Hj /= ?; subst j. exfalso. by rewrite ltnNge leq_addr in Hj. + case=> j Hj /= /eqP. rewrite eqn_add2l => /eqP ?; subst j. by rewrite !mxE. rewrite 2!mxE !castmxE /= F2_mx_opp !cast_ord_id !mxE. case: splitP. - case=> j Hj /= ?; subst j. case: splitP. + case=> j Hj_ /= ?; subst j. by rewrite !mxE. + case=> k Hk /= ?; subst i. exfalso. by rewrite ltnNge leq_addr in Hj. - case=> k Hk /= ?; subst i. case: splitP. + case=> j Hj /= ?; subst j. exfalso. by rewrite ltnNge leq_addr in Hj. + case=> j Hj /= /eqP. rewrite eqn_add2l => /eqP ?; subst j. rewrite mxE [in X in _ = X]mxE castmxE /= cast_ord_id. congr (CSM _ _); exact: val_inj. 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