proposition: Lemma hemi_comp_graph_eqP : Equality.axiom hemi_comp_graph_eqb.
proof: Proof. case => p1 pp1 b1 po1 bp1. case => p2 pp2 b2 po2 bp2. rewrite /hemi_comp_graph_eqb /=. case: eqP => Hp /=. case: eqP => Hb /=. eapply ReflectT. destruct Hp. destruct Hb. subst po1 po2. by rewrite (eq_irrelevance bp1 bp2) (eq_irrelevance pp1 pp2). apply ReflectF => [] [] _. by move/Hb. apply ReflectF => [] []. by move/Hp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner