proposition: Lemma colorable_tanner_rel : colorable tanner_rel tanner_rel_kind.
proof: Proof. rewrite tanner_relE; by case => v1; case. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition