proposition: Lemma step_dist_it_ge0 c r t : r >= 0 -> (step_dist_it c r t).2 >= 0.
proof: Proof. elim: t c r => [|a t IHt] c r Hr; rewrite /step_dist_it /=. by case: (enum _). case: (enum _) => //. move=> b l /=. elim: (zip l t) (step_dist c r b a) (step_dist_ge0 c b a Hr) => [] //= [b' a'] l' IH r' Hr'. by rewrite IH // step_dist_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner