proposition: Lemma connected_switch : partial_connected c -> partial_connected (switch c).
proof: Proof. move=> Hc x y Hx Hy. case: (Hc (switch_graph_node x) (switch_graph_node y)). - by destruct x. - by destruct y. - move => p [b1 [b2 /andP [Hp Hl]]]. exists (map switch_path_node p), b1, b2. rewrite -(switch_graph_nodeK x). rewrite -/(switch_path_node (switch_graph_node x, b1)). rewrite (@map_path _ _ _ _ (graph_rel c) pred0); first last. by rewrite has_pred0. move=> a b _. by rewrite switch_graph_rel. rewrite Hp /=. rewrite last_map (eqP Hl). by rewrite /switch_path_node switch_graph_nodeK. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner