proposition: Lemma border_nodes_step_it c t : t \in dest_ports c #|border (nodes c)| -> border (nodes (step_it c t)) = set0.
proof: Proof. remember (#|border (nodes c)|) as k. elim: k c t Heqk => [|k IH] c t eqk. rewrite tuple0 /step_it. case: cardEP (eqk) => //= _ _. by apply cards0_eq. rewrite (dest_ports_step def_port); last by rewrite -eqk. move/bigcupP => [/= i Hi]. move/imsetP => [t' Ht' ->] /=. rewrite /step_it /=. move: eqk Ht' (@enum_step_border c). case: cardEP => //= s b [] eqk Ht' /(_ s b) Hesb. move: (IH (step c s i.1 i.2) t'). rewrite /step_it cardE Hesb //. by apply. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner