proposition: Lemma sum_step_border : \sum_(i in dest_port | i.1 \in border (conodes c)) dest_dist i.2 = #|border (conodes c)|%:R.
proof: Proof. rewrite -sum1_card /dest_port. transitivity (\sum_(x : port * {set port} | [&& x.1 \in border (conodes c), x.1 \in x.2 & trivIset (x.2 |: conodes c)]) dest_dist x.2). apply eq_bigl => i /=. rewrite andbC in_set !andbA. case Hb: (_ \in border _) => //=. by rewrite /free_coports !inE Hb. rewrite -(pair_big_dep _ (fun x (y : {set port}) => (x \in y) && trivIset (y |: conodes c)) (fun x => dest_dist)) /=. transitivity (\sum_(i in border (conodes c)) (1:K)). apply eq_bigr => i Hi. move/subsetP/(_ _ Hi): (border_p (conodes c)) => /bigcupP [s Hs His]. rewrite (big_pred1 s) ?dest_dist1 //. move=> s' /=. case: eqP => Hs'. rewrite Hs' His /=. apply trivIset_in => //. by apply part_p. case His': (i \in s') => //=. apply/trivIsetP => /(_ s' s). rewrite !inE eqxx Hs orbT /=. move/eqP in Hs'. move/(_ erefl erefl Hs')/disjoint_setI0/setP/(_ i). by rewrite !inE His His'. by rewrite sum1_card sumr_const. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner