proposition: Lemma add_edge_step_it c p t ep en : (index p (enum (border (nodes c))) < #|border (nodes c)|)%nat -> t \in dest_ports c #|border (nodes c)| -> nth (def_port, set0) t (index p (enum (border (nodes c)))) = (ep, en) -> p \in edom (step_it c t) /\ (edges (step_it c t)) p = ep.
proof: Proof. destruct t as [t Hsz]. move: Hsz. rewrite /step_it cardE /=. elim: t c => [|t0 t IH] /= c. move=> Hsz Hidx. by rewrite -(eqP Hsz) ltn0 in Hidx. set eb := enum _. case_eq eb => // s b Hb Hsz Hidx. rewrite (dest_ports_step def_port); last first. by rewrite cardE -/eb Hb. move=> /bigcupP /= [y] Hy. move/step_dest_port: (Hy). move/(_ s). rewrite -mem_enum -/eb Hb inE eqxx => /(_ erefl) /andP [Htriv Hcond]. move/imsetP => /= [x Hx] [] ? ?. subst t0 t. move: Hidx => /=. case: ifP => /eqP Hs /= Hidx Hy'. subst y s => /=. have : edges (step c p ep en) p = ep := step_edges_sp_ep Htriv Hcond. have : p \in edom (step c p ep en) := sp_in_step_edom Htriv Hcond. clear. elim: (zip _ _) (step c _ _ _) => // a z IH c' Hp' He. destruct (IH (step c' a.1 a.2.1 a.2.2)) => //. apply/subsetP: Hp'. by apply monotonic_edom_step. by rewrite monotonic_edges_step. rewrite -[in B in zip B x](enum_step_border Hb Hy) //=. move/eqP: Hsz => []. rewrite -[in RHS](enum_step_border Hb Hy) => /eqP Hsz. apply (IH _ Hsz); rewrite ?(enum_step_border Hb Hy) //. destruct x. rewrite (enum_step_border Hb Hy) in Hsz *. by rewrite (eq_irrelevance Hsz i). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner