fact: Hypothesis BEC_y : exists c : 'rV['F_2]_n, c BEC( H ) y.
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