proposition: Lemma switch_edges_cancel : {in edom c, cancel (edges c) switch_edges}.
proof: Proof. move=> x Hx. rewrite /switch_edges ffunE. rewrite /switch_edom -(edom_codom c). rewrite imset_f //. case: pickP. move=> y /andP [/eqP Hyx Hyc]. by rewrite (edges_inj Hyc Hx Hyx). move/(_ x). by rewrite eqxx Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner