proposition: Lemma dest_ports_step c len : #|border (nodes c)| != 0%nat -> dest_ports c len.+1 = \bigcup_(x in dest_port c) cons_tuple x @: dest_ports (step c (bnext c) x.1 x.2) len.
proof: Proof. rewrite -curry_imset2l_dep => Hb. rewrite /dest_ports /=. symmetry. apply/setP => t. apply/imset2P. case: ifP => Ht /=. - destruct t as [x Hszx]. destruct x as [|x s] => //. have Hs := Hszx; rewrite eqSS in Hs. move: Ht. rewrite inE /= => /and3P [] /andP [] Hxin Hin /andP [Hunx Hun] Htriv. have Hx: x \in dest_port c. move: Hxin => /=. rewrite !inE => /andP [Hout Hx]. rewrite Hx Hout /=. apply/trivIsetS: Htriv. apply/setSU/subsetP => /= i. by rewrite !inE => ->. have Hmem0: bnext c \in border (nodes c). move: Hb. rewrite cardE -mem_enum /bnext. case: (enum _) => //= a l _. by rewrite in_cons eqxx. move: (step_dest_port Hmem0 Hx) => {Hmem0} /andP [Htrivx Hcond]. exists x (Tuple Hs). + exact Hx. + rewrite inE Hun. apply/andP; split. apply/allP => /= i Hi. rewrite step_codom_ok //. move/allP/(_ i Hi): Hin. rewrite !inE negb_or -andbA => ->. rewrite andbT. move: Hunx; apply contra => /eqP Heq. by rewrite -Heq map_f // mem_nth // (eqP Hs). apply/trivIsetP => A B. rewrite step_conodes_ok //. rewrite !inE /= => HA HB HAB. by apply (trivIsetP Htriv) => //; rewrite !inE (orbC (_ == x.2)) -orbA. + by apply: val_inj. - move=> [/= x t' Hx Ht' Htt']. move/negP: Ht; apply. subst t. move: Ht'. destruct t' as [t Ht] => /=. rewrite inE /= => /and3P[Hin Hun Htriv]. rewrite inE in Hx. rewrite inE. move/and3P: (Hx) => [Hx1 Hx2 Htrivx]. have Hcond: step_cond c (bnext c) x.1 x.2. apply/andP; split. rewrite /step_start_cond. move: Hb. rewrite cardE -mem_enum /bnext. case: (enum (border (nodes c))) => //= a l _. by rewrite in_cons eqxx. by rewrite /step_end_cond inE -in_setC Hx1 Hx2. rewrite step_codom_ok // in Hin. apply/and3P; split. - apply/allP=> /= i. rewrite inE => /orP [/eqP ->|Hi]. by rewrite inE -in_setC Hx1 Hx2. move/allP/(_ _ Hi): Hin. by rewrite !inE negb_or -andbA => /andP [_]. - rewrite /= Hun andbT. apply/negP => /mapP [y Hy Hxy]. move/allP/(_ _ Hy): Hin. by rewrite -Hxy !inE eqxx. - apply/trivIsetP => A B. rewrite /= => HA HB HAB. have Hsub: [set y in x.2 :: unzip2 t] :|: conodes c \subset [set y in unzip2 t] :|: step_conodes c (bnext c) x.1 x.2. apply/subsetP => X. rewrite !inE step_conodes_ok // !inE orbA /=. by rewrite (orbC (X == _)). by apply (trivIsetP Htriv) => //; apply (subsetP Hsub). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner