proposition: Lemma switchK_edges : switch_edges (switch c) = edges c.
proof: Proof. apply/ffunP => p. rewrite /switch_edges /switch ffunE /=. case: ifP => Hp. case: pickP => /=. move=> x. rewrite /edom /=. rewrite -edom_codom => /andP [/eqP Hx] /imsetP [y Hy Hxy]. rewrite Hxy switch_edges_cancel // in Hx. by rewrite -Hx. move/(_ (edges c p)). rewrite switch_edges_cancel // eqxx /=. by rewrite /edom -edom_codom imset_f. by rewrite edges_out // inE Hp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner