proposition: Lemma weighted_count_switch_ge0 P lam rho c c' r i l : r > 0 -> weighted_count P [seq switch_step_dist_it lam rho c r (i :: tval y) | y in dest_ports_seqs c' l] >= 0.
proof: Proof. rewrite /weighted_count big_map => Hr. by apply sumr_ge0 => ? _; rewrite switch_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