proposition: Lemma step_dist_ge0 c r b a : r >= 0 -> (step_dist c r b a).2 >= 0.
proof: Proof. move=> Hr; rewrite /step_dist /=. rewrite -mulrA mulr_ge0 // mulr_ge0 // ?dest_dist_ge0 //. by rewrite invr_ge0 ler0n. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner