proposition: Lemma monotonic_switch_progress f (c : comp_graph port) : edom c \subset edom (f c) -> {in edom c, edges (f c) =1 edges c} -> graph_dom (conodes c) \subset graph_dom (conodes (f c)) /\ {in graph_dom (conodes c), switch_edges (f c) =1 switch_edges c}.
proof: Proof. move => Hsub He. split. rewrite -2!edom_codom. rewrite -(eq_in_imset He). by apply imsetS, Hsub. move=> // ep. rewrite -edom_codom => /imsetP [p Hp ->] {ep}. rewrite -[in LHS](He _ Hp). rewrite !switch_edges_cancel //. apply/subsetP: Hp; apply Hsub. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner