proposition: Lemma switch_edges_inj : {in switch_edom &, injective switch_edges}.
proof: Proof. rewrite /switch_edom -(edom_codom c). move=> x y. move/imsetP => [x0 Hx0 ->]. move/imsetP => [y0 Hy0 ->]. by rewrite !switch_edges_cancel // => ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner