proposition: Lemma iSP_BEC0_Blank : forall l m0 n0, m0 \notin 'F n0 -> (iSP_BEC0 l) m0 n0 = Blank.
proof: Proof. elim=> [m0 n0 m0n0 | l IH m0 n0 m0n0]; by rewrite /= !mxE (negbTE m0n0) ?IH. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode