proposition: Lemma tanner_relE : tanner_rel = tanner_rel'.
proof: Proof. by rewrite /tanner_rel; unlock. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition