proposition: Lemma PCM_instanceE n0 m0 y : m0 \in 'F n0 -> (PCM_instance y) m0 n0 = y ``_ n0.
proof: Proof. move=> m0n0; by rewrite /mxSum !mxE m0n0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) f2 ssr_ext ssralg_ext max_subset num_occ hamming ldpc_erasure tanner linearcode