proposition: Lemma SP_BEC0_is_a_fixpoint : SP_BEC0 = mxSum H (mxProd H y SP_BEC0).
proof: Proof. rewrite /SP_BEC0; by case: SP_BEC0_rec => H' []. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext ssralg_ext num_occ f2 ssrR hamming tanner linearcode