proposition: Lemma switch_graph_rel x y : graph_rel (switch c) (switch_path_node x) (switch_path_node y) = graph_rel c x y.
proof: Proof. rewrite /graph_rel /switch /switch_path_node /switch_graph_node. destruct x, y, g, g0, b, b0 => //=; by rewrite graph_rel_switch. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner