proposition: Lemma weighted_count_it_ge0 i r k P c c' : 0 < r -> 0 <= weighted_count P [seq step_dist_it c r (i :: tval y) | y in dest_ports c' k].
proof: Proof. rewrite /weighted_count big_map => ?. apply sumr_ge0 => ? _; by rewrite step_dist_it_ge0 // ltW. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner