proposition: Lemma ports_conodes_step_it lam c r k t len : t \in dest_ports c k -> (step_dist_it lam c r t).2 != 0 -> (size lam <= maxdeg -> #|ports (nodes c)| <= len -> #|known_coports c| <= len -> #|known_coports (step_it c t)| <= len * maxdeg.+1)%nat.
proof: Proof. clear -def_port. move=> Ht Hr2 Hlam. move/(leq_trans (card_border_ports _)). rewrite mulnS. rewrite cardE => Hp Hcp. apply (@leq_trans (len + size (enum (border (nodes c))) * maxdeg)). move: {Hp} Ht Hr2 Hcp. elim: k r len c t => [|k IH] //= r len c t. move=> Ht Hr Hcp. rewrite tuple0 /step_it /=. apply (@leq_trans len). by destruct (enum _) => /=. by apply leq_addr. remember (enum (border (nodes c))) as b. rewrite /step_it -Heqb. destruct b => /=. by rewrite zip_nill mul0n addn0. rewrite mulSn addnA. rewrite (dest_ports_step def_port) /=; last first. by rewrite cardE -Heqb. move/bigcupP => [/= i Hi]. move/imsetP => [t' Ht' ->] /=. rewrite -(enum_step_border (esym Heqb) Hi). move=> Hr Hcp. have Hsb: s \in border (nodes c). by rewrite -mem_enum -Heqb inE eqxx. apply (IH (step_dist lam c r s i).2). by rewrite -Heqb /= in Ht'. move: Hr; rewrite /step_dist_it -Heqb /=. by rewrite (enum_step_border (esym Heqb) Hi). rewrite /=. move/andP: (step_dest_port Hsb Hi) => [Hcond Htriv]. rewrite /known_coports step_coports_ok //. case /boolP: (i.2 \in conodes c) => Hi2. rewrite eq_setSU. by apply (leq_trans Hcp), leq_addr. apply/subsetP => j Hj. by apply/bigcupP; exists i.2. rewrite cardsU addnC. apply (leq_trans (leq_subr _ _)). apply leq_add => //. rewrite /step_dist_it -Heqb /= in Hr. set cr' := step_dist _ _ _ _ _ in Hr. case/boolP: (cr'.2 == 0) => Hr'. rewrite -(enum_step_border (esym Heqb) Hi) in Hr. move: (step_dist_it_const lam cr'.1 cr'.2 t'). rewrite {1}/step_dist_it -surjective_pairing => Hc. move: Hr. rewrite Hc (eqP Hr'). destruct step_dist_it => /=. by rewrite mul0r eqxx. rewrite /= in Hr'. case/boolP: (dest_dist lam c i.2 == 0) => Hdi. by rewrite (eqP Hdi) mulr0 mul0r eqxx in Hr'. by apply (cards_conode_out Hlam Hdi). by rewrite leq_add2l leq_mul2r Hp orbT. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner