proposition: Lemma step_dist_it_const c r y : step_dist_it c r y = let (c', r') := step_dist_it c 1 y in (c', r * r').
proof: Proof. rewrite /step_dist_it. move: (enum _) (free_coports c) => s1 f. elim: (zip s1 y) r c => [|a s IHs] r c /=. by rewrite mulr1. rewrite /step_dist. rewrite IHs mul1r. rewrite (IHs (_ / _)). case: (foldl _ _ _) => a' b. by rewrite !mulrA. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner