proposition: Lemma weighted_count_next (P : pred ({set port} * comp_graph port)) : weighted_count P next_graphs = \sum_(pn | start_dist pn != 0) weighted_count (fun c => P (pn,c)) [seq switch_step_dist_it lam rho (start_graph pn) (start_dist pn) (tval seqs) | seqs in dest_ports_seqs def_port (start_graph pn) l].
proof: Proof. rewrite /weighted_count big_map big_mkcond big_enum_in /build_traces /=. rewrite curry_imset2l_dep. rewrite partition_disjoint_bigcup /=; last first. move=> i j Hij. rewrite disjoints_subset. apply/subsetP => x /imsetP [y Hy ->] {x}. rewrite inE. apply/negP => /imsetP [z Hz] [] /eqP. by rewrite (negbTE Hij). rewrite (bigID (fun i => start_dist i == 0)) big1 /= ?add0r; last first. move=> i Hi. rewrite big_imset /=. rewrite big1 // => j Hj. case: ifP => _ //. rewrite /graph_of_trace (eqP Hi) switch_step_dist_it_const. destruct switch_step_dist_it. by rewrite mul0r. by move => a b _ _ []. apply eq_bigr => i Hi. rewrite big_imset /=; last first. by move => a b _ _ []. rewrite big_map [RHS]big_mkcond big_enum_in /=. apply eq_bigr => j Hj /=. rewrite /graph_of_trace /=. by destruct switch_step_dist_it. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner