proposition: Lemma weighted_count_step c r len P : (#|border(nodes c)| > len)%nat -> weighted_count P [seq step_dist_it c r (tval dests) | dests in dest_ports c len.+1] = \sum_(x in dest_port c) weighted_count P [seq step_dist_it c r (cons_tuple x y) | y in dest_ports (step c (bnext c) x.1 x.2) len ].
proof: Proof. move=> Hlen. rewrite dest_ports_step; last first. rewrite -lt0n. by apply (leq_ltn_trans (leq0n len)). rewrite /weighted_count big_map. rewrite big_mkcond /=. rewrite [in enum _]big_mkcond /=. rewrite big_enum_in /= 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 _ _)). destruct x, y => /= /eqP. rewrite eqseq_cons => /andP [/eqP Hij']. by rewrite Hij' eqxx in Hij. by rewrite disjoint_sym disjoints_subset sub0set. by rewrite disjoints_subset sub0set. rewrite /bnext. case: cardEP Hlen => // s b _. symmetry. rewrite big_mkcond /=. apply eq_bigr => i _. case: ifP => Hif. rewrite big_map big_mkcond /= big_enum_in /= big_imset //=. by move=> u v _ _; apply cons_tuple_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