proposition: Lemma sum_step_used : \sum_(i in dest_port | (i.1 \in known_coports c) && (i.1 \notin border (conodes c))) dest_dist i.2 = 0.
proof: Proof. rewrite big1 // => i /andP [] /=. rewrite !inE => /andP [Hp] _ /andP [Hi1 Hi2]. by rewrite Hi1 Hi2 in Hp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner