proposition: Lemma weighted_count_switch_step l c r lam rho P : weighted_count P [seq switch_step_dist_it lam rho c r (tval seqs) | seqs in dest_ports_seqs c l.+1] = \sum_(t in dest_ports c #|border (nodes c)|) weighted_count P [seq switch_step_dist_it lam rho c r (tuple_to_partial (def_port, set0) t :: tval y) | y in dest_ports_seqs (switch (step_it c t)) l].
proof: Proof. rewrite dest_ports_seqs_step. rewrite /weighted_count big_map big_enum_in [LHS]/=. rewrite big_mkcondr [\bigcup_(_ in _) _]big_mkcond /=. rewrite partition_disjoint_bigcup /=; last first. move=> i j Hij. case: ifP => Hi. case: ifP => Hj. rewrite disjoints_subset. apply/subsetP => a /imsetP [x Hx ->] {a}. rewrite inE. apply/negP => /imsetP [y Hy]. move/(f_equal (@tval _ _)) => /eqP. rewrite eqseq_cons => /andP [] /eqP. move/(f_equal (@partial_to_tuple _ (border (nodes c)) _)). rewrite !tuple_to_partialK => /eqP. by rewrite (negbTE Hij). by rewrite disjoint_sym disjoints_subset sub0set. by rewrite disjoints_subset sub0set. symmetry. rewrite big_mkcond /=. apply eq_bigr => i _. case: ifP => Hif. rewrite big_map big_mkcond /= big_enum_in /=. rewrite big_imset //. move=> u v _ _. destruct u as [u Hu], v as [v Hv] => /= Heq. apply (f_equal (@tval _ _)) in Heq. move: Heq => [] Heq. by apply val_inj. by rewrite big_set0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner