proposition: Lemma switch_edom_codom : switch_edges @: switch_edom = edom c.
proof: Proof. apply/setP => x. rewrite /switch_edom -edom_codom. apply/imsetP. case: ifP => Hx. - exists (edges c x). by rewrite imset_f. by rewrite switch_edges_cancel. - move => [y Hy Hxy]. move/imsetP: Hy => [x' Hx' Hyx']. rewrite Hyx' switch_edges_cancel // in Hxy. by rewrite Hxy Hx' in Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner