proposition: Lemma simple_tanner_rel : simple tanner_rel.
proof: Proof. exact/(@colorable_is_simple _ tanner_rel 2)/colorable_tanner_rel. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition