proposition: Lemma switch_edges_out : {in ~: switch_edom, switch_edges =1 ssrfun.id}.
proof: Proof. rewrite /switch_edges => x Hx. rewrite ffunE. case: ifP => // Hx'. by rewrite inE Hx' in Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner