proposition: Lemma lel_mat_erase (c : 'rV['F_2]_n) E : map_mx Bit c <=m erase c E.
proof: Proof. apply/'forall_forallP => /= m0 n0; rewrite (ord1 m0){m0}. rewrite 2!mxE; case: ifPn => // n1E; by rewrite lell. 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