proposition: Lemma sum_step_out : \sum_(i in dest_port | i.1 \notin known_coports c) dest_dist i.2 = (#|port| - #|known_coports c|)%:R.
proof: Proof. rewrite /dest_port. transitivity (\sum_(x : port * {set port} | [&& x.1 \notin known_coports c, x.1 \in x.2 & trivIset (x.2 |: conodes c)]) dest_dist x.2). apply eq_bigl => i /=. rewrite andbC in_set !andbA !inE. case Hb: (_ \in ports _) => //=. by rewrite andbF. rewrite -(pair_big_dep (fun x => x \notin known_coports c) (fun x (y : {set port}) => (x \in y) && trivIset (y |: conodes c)) (fun x => dest_dist)) /=. transitivity (\sum_(i in port | i \notin known_coports c) (1:K)); last first. by rewrite sumr_const -cardsE cardsCp. apply eq_bigr => i Hi. by rewrite dest_dist_out. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner