proposition: Lemma switch_step_dist_it_const lam rho c r y : switch_step_dist_it lam rho c r y = let (c', r') := switch_step_dist_it lam rho c 1 y in (c', r * r').
proof: Proof. elim: y lam rho c r => [|t y IH] lam rho c r /=. by rewrite mulr1. rewrite step_dist_it_const /=. destruct step_dist_it. rewrite IH [in RHS]IH. destruct switch_step_dist_it. by rewrite mulrA. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner