proposition: Lemma weighted_count_it_eq0 i r k c : enum (border (nodes c)) != [::] -> dest_dist c i.2 == 0 -> weighted_count predT [seq step_dist_it c r (i :: tval y) | y in dest_ports (step c (bnext c) i.1 i.2) k] = 0.
proof: Proof. move=> ? ?; by rewrite /weighted_count sum_step_dist_it_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner