proposition: Lemma monotone_conodes_switch_step_it l c (ts : l.*2.-tuple _) : conodes c \subset conodes (switch_step_it c ts).
proof: Proof. elim: l c ts => [|l IH] c ts. by rewrite tuple0. case: ts => [] [|t1] // [|t2 ts] //=. rewrite doubleS => /eqP [] /eqP Hsz. rewrite (subset_trans _ (IH _ (Tuple Hsz))) //=. rewrite part_nodes_step_it /=. apply monotone_conodes_step_it. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner