proposition: Lemma sum_weighted_count_it c r k s b P : enum (border (nodes c)) = s :: b -> s \in border (nodes c) -> (forall (c : comp_graph port) (r : K), k <= #|border (nodes c)| -> k * maxdeg < #|port| - #|known_coports c| -> weighted_count predT [seq step_dist_it c r (tval y) | y in dest_ports c k] = r)%nat -> (k < #|border (nodes c)|)%nat -> (k.+1 * maxdeg < #|port| - #|known_coports c|)%nat -> (maxdeg <= #|port| - #|known_coports c|)%nat -> \sum_(x in dest_port c | P x) weighted_count predT [seq step_dist_it c r (x :: tval y) | y in dest_ports (step c (bnext c) x.1 x.2) k] = \sum_(x in dest_port c | P x) (step_dist c r s x).2.
proof: Proof. move=> Heqb Hhead IHk Hb Hk Hlam. apply/eq_bigr => x /andP [Hx _]. case Hr'0: (dest_dist c x.2 == 0). by rewrite /= (eqP Hr'0) mulr0 mul0r weighted_count_it_eq0 // Heqb. rewrite /step_dist_it Heqb /=. remember (step_dist c r s x) as cr. move: cr Heqcr => [c' r'] [] -> Hr' /=. rewrite -Hr'. move: IHk; rewrite /step_dist_it. rewrite /bnext Heqb -(enum_step_border Heqb Hx) /=. apply. rewrite /= /step_nodes. rewrite (step_dest_port _ Hx) //=. by rewrite (cardsD1 s) Hhead add1n /= ltnS in Hb. move/negbT in Hr'0. by apply free_step_coports_gt. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner