proposition: Lemma switch_edges_cancel2 : {in switch_edom, cancel switch_edges (edges c)}.
proof: Proof. move=> x Hx. have Hxc: switch_edges x \in edom c by rewrite -switch_edom_codom imset_f. apply switch_edges_inj => //. by rewrite /switch_edom -edom_codom imset_f. 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