proposition: Lemma free_step_coports_gt c k s x : (k.+1 * maxdeg < #|port| - #|known_coports c|)%nat -> s \in border (nodes c) -> x \in dest_port c -> dest_dist c x.2 != 0 -> (k * maxdeg < #|port| - #|known_coports (step c s x.1 x.2)|)%nat.
proof: Proof. move=> Hk Hhead Hx Hr'0. have/andP [Htriv Hcond] := step_dest_port Hhead Hx. rewrite /known_coports /= step_coports_ok //. rewrite /ports /=. case/boolP : (x.2 \in conodes c) => Hx2. rewrite eq_setSU. rewrite mulSn addnC in Hk. by rewrite -(leq_add2r maxdeg) (leq_trans Hk) // leq_addr. by apply/subsetP => y Hy; apply/bigcupP; exists x.2. rewrite cardsU disjoint_setI0; last first. rewrite disjoint_sym disjoints_subset. apply/subsetP => i Hip. rewrite inE; apply/negP => Hix2. by rewrite (trivIset_I1 Htriv Hix2 Hip) in Hx2. rewrite cards0 subn0 addnC subnDA. rewrite mulSn addnC in Hk. apply (leq_sub2r maxdeg) in Hk. rewrite -addSn addnK in Hk. apply (leq_trans Hk). apply leq_sub2l. by apply (cards_conode_out Hr'0). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner