proposition: Lemma graph_rel_irrel : nodes c' = nodes c /\ conodes c' = conodes c /\ edges c' = edges c -> graph_rel c' =2 graph_rel c.
proof: Proof. move=> [Hn [Hcn He]] x y. by rewrite /graph_rel /edom Hn Hcn He. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner