proposition: Lemma weighted_count_it c r k : (k <= #|border (nodes c)|)%nat -> (k * maxdeg < #|port| - #|known_coports c|)%nat -> weighted_count predT [seq step_dist_it c r (tval y) |y in dest_ports c k] = r.
proof: Proof. elim: k c r => /= [|k IHk] c r Hb Hk. rewrite dest_ports_0 /=. rewrite /image_mem enum_set1 /step_dist_it /=. rewrite /weighted_count big_seq1. by case: (enum _). rewrite weighted_count_step //. move: (Hb); rewrite cardE. move eqb : (enum (border (nodes c))) => [//|s b]. have Hhead: s \in border (nodes c). by rewrite -mem_enum eqb inE eqxx. have Hlam: (maxdeg <= #|port| - #|known_coports c|)%nat. rewrite mulSn in Hk. apply ltnW in Hk. by rewrite -(leq_add2r (k * maxdeg)) (leq_trans Hk) // leq_addr. rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. rewrite (sum_weighted_count_it r predT eqb) //. move: (weight_is_dist Hhead (leq_trans Hmax Hlam)). rewrite /weighted_count big_map big_enum_in /=. rewrite (bigID xpredT) /= [in X in _ + X]big_pred0 ?addr0; last first. by move=> ?; rewrite andbF. rewrite -!big_distrl -!big_distrr /= mul1r -mulrA => ->. by rewrite mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner