proposition: Lemma switch_step_dist_it_1 lam rho c r ts : (switch_step_dist_it lam rho c r ts).1 = switch_step_it c ts.
proof: Proof. elim: ts lam rho c r => //= t ts IH lam rho c r. rewrite -(step_dist_it_1 lam c r). by destruct step_dist_it. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner