proposition: Lemma sum_step_dist_it_eq0 c c' (i : port * {set port}) k r : enum (border (nodes c)) != [::] -> dest_dist c i.2 == 0 -> \sum_(xw <- [seq step_dist_it c r (i :: tval y) | y in dest_ports c' k]) xw.2 = 0.
proof: Proof. move=> Heqb Hd. have {Heqb}[s [b Heqb]] : exists s b, s :: b = enum (border (nodes c)). case: (enum _) Heqb => // s b _; by exists s, b. rewrite /step_dist_it /= /bnext -Heqb /=. rewrite big_map /= big1 // => j _. rewrite /(step_dist c r s i) (eqP Hd) /= mulr0 mul0r. move: (zip b j) (step c _ _ _). clear. elim => //= a l IH c. by rewrite /step_dist !mul0r IH. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner