fact: Definition test_mat : 'M['F_2]_(4, 4) := \matrix_(i < 4, j < 4) if j == 0 then 1 else if j == 1 then 1 else 0.
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