proposition: Lemma switch_step_it_cat c ts1 ts2 : switch_step_it c (ts1 ++ ts2) = switch_step_it (switch_step_it c ts1) ts2.
proof: Proof. by elim: ts1 c => //=. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner