proposition: Lemma conodes_step_it c t : t \in dest_ports c #|border (nodes c)| -> tree_like (step_it c t) -> partial_connected c -> [set y in unzip2 t] :|: conodes c = conodes (step_it c t) /\ border (conodes (step_it c t)) = border (conodes c) :|: \bigcup_(i <- t) (i.2 :\ i.1).
proof: Proof. remember (#|border (nodes c)|) as k. elim: k c t Heqk => [|k IH] c t eqk. rewrite tuple0 /step_it zip_nilr /=. by rewrite big_nil // set_nil set0U setU0. rewrite (dest_ports_step def_port); last by rewrite -eqk. move/bigcupP => [/= i Hi]. move/imsetP => [t' Ht' ->] Htl Hpc /=. rewrite /step_it /=. remember (enum _) as b0. move: (Heqb0) eqk (@enum_step_border c). case: cardEP => //= s b Heqb [] eqk /(_ s b i erefl Hi) Hesb. subst b0. rewrite big_cons set_cons setUAC setUC. have Htl': tree_like (step_it (step c s i.1 i.2) t'). by move: Htl; rewrite /step_it /= Heqb /= Hesb. destruct (IH (step c s i.1 i.2) t') as [Hc Hb]. + rewrite /step_it cardE Hesb. + by []. + by rewrite Heqb in Ht'. + by []. + by apply connected_step. have Hin: s \in s :: b by rewrite in_cons eqxx. rewrite -Heqb mem_enum in Hin. have /andP[Htriv Hcond] := step_dest_port Hin Hi. split. move: Hc; rewrite /step_it /= Heqb Hesb. by rewrite step_conodes_ok. move: Hb; rewrite /step_it Heqb Hesb. rewrite setUA step_coborder_ok //. move/andP: (Hcond); rewrite /step_end_cond inE => [] [_] /andP [_ Hi12]. case: ifP => Hi2. move: (tree_like_no_sharing Hin Hpc Htriv Hcond (tree_like_rev_step_it Htl')). move/negP; elim. by apply/bigcupP; exists i.2. rewrite setDUl. have -> // : border (conodes c) :\ i.1 = border (conodes c). apply/setP => x. rewrite !inE. case: eqP => Hx //. case Hx': (x \in border _) => //. rewrite (trivIset_I1 Htriv Hi12) // in Hi2. rewrite -Hx. by apply/subsetP: Hx'; apply border_p. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner