fact: Variables (n m : nat) (H : 'M['F_2]_(m, n)) (A : {set 'I_n}).
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix vector) Reals ssralg_ext ssrR Reals_ext f2 fdist channel tanner linearcode pproba