proposition: Lemma comp_graph_eqP : Equality.axiom comp_graph_eqb.
proof: Proof. case => n1 cn1 e1 ed1 ec1 ei1 eo1. case => n2 cn2 e2 ed2 ec2 ei2 eo2. rewrite /comp_graph_eqb /=. case: eqP => Hn /=. case: eqP => Hcn /=. case: eqP => He /=. eapply ReflectT. destruct Hn, Hcn, He. subst ed1 ed2. rewrite (eq_irrelevance ec1 ec2). have -> : ei1 = ei2 by apply boolp.Prop_irrelevance. have -> : eo1 = eo2 by apply boolp.Prop_irrelevance. by []. apply ReflectF => [] [] _ _. by move/He. apply ReflectF => [] [] _. by move/Hcn. apply ReflectF => [] []. by move/Hn. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner