proposition: Lemma step_coborder : let cn := conodes c in ((border cn :|: if end_node \in cn then set0 else end_node) :\ end_port) \subset (\bigcup_(x in end_node |: conodes c) x).
proof: Proof. rewrite /=. case: ifP => Hend. - rewrite setU0. apply/subsetP => x. rewrite bigcup_setU in_setU. rewrite in_setD => /andP [_ Hx]. by rewrite (subsetP (border_p (conodes c)) _ Hx) orbT. - apply/subsetP => x. rewrite bigcup_setU in_setU. rewrite in_setD => /andP [Hx1]. rewrite in_setU => /orP [] Hx2. by rewrite (subsetP (border_p (conodes c)) _ Hx2) orbT. apply/orP; left. apply/bigcupP; exists end_node; last by []. by rewrite in_set eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner