proposition: Lemma monotonic_switch_step_it c l (ts : l.*2.-tuple _) : edom c \subset edom (switch_step_it c ts) /\ {in edom c, edges (switch_step_it c ts) =1 edges c}.
proof: Proof. elim: l ts => [|l IHl] ts. rewrite tuple0 /=. by split; [apply subxx | move => ? ?]. rewrite doubleS -addn2 addnC in ts *. case: ts => /=. apply: last_ind => // ts t1 _. rewrite size_rcons /= => /eqP [] Hsz. move: ts Hsz. apply: last_ind => // ts t2 _. rewrite size_rcons /= => [] [] Hsz. rewrite -cats1 /= switch_step_it_cat. move/eqP in Hsz. move/(_ (Tuple Hsz)) => /= in IHl. have Hsw : {in edom c, switch_edges (switch_step_it c (rcons ts t2)) =1 edges c}. rewrite -cats1 switch_step_it_cat /= switchK_edges => p Hp. rewrite monotonic_edges_step_it => //. + by apply IHl. + apply/subsetP: Hp. by apply IHl. have Hsw' : edom c \subset graph_dom (conodes (switch_step_it c (rcons ts t2))). apply (subset_trans (proj1 IHl)). rewrite -cats1 switch_step_it_cat /=. by apply monotonic_edom_step_it. split. rewrite /= /edom /=. by rewrite (subset_trans _ (monotonic_codom_step_it _ _)). move=> /= p Hp. rewrite monotonic_switch_edges_step_it. by rewrite Hsw. by apply/subsetP: Hp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner