proposition: Lemma switch_step_dist_it_ge0 lam rho c r y : r >= 0 -> (switch_step_dist_it lam rho c r y).2 >= 0.
proof: Proof. elim: y lam rho c r => //= a y IHy lam rho c r Hr. set d := map _ _. move: (step_dist_it_ge0 lam c d Hr). case: (step_dist_it _ _ _) => /= c' r'. by apply IHy. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner