proposition: Lemma graph_rel_switch x y : (y \in graph_dom (conodes c)) && (switch_edges c y == x) = (x \in edom c) && (edges c x == y).
proof: Proof. case Hx: (x \in _) => /=. case Hxy: (edges c x == y). rewrite -(eqP Hxy) switch_edges_cancel // eqxx andbT. by rewrite -edom_codom imset_f. case Hy: (y \in _) => //=. case Hyx: (_ == _) => //. by rewrite -(eqP Hyx) switch_edges_cancel2 // eqxx in Hxy. case Hy: (y \in _) => //=. case Hyx: (_ == _) => //. rewrite -switch_edom_codom -(eqP Hyx) in Hx. by rewrite imset_f in Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner