proposition: Lemma cards_conode_out (c : comp_graph port) (s : {set port}) : dest_dist c s != 0 -> s \notin conodes c -> (#|s| <= maxdeg)%nat.
proof: Proof. move=> Hn0 Hs. rewrite /dest_dist (negbTE Hs) in Hn0. case Hlam': (lambda`_#|s|.-1 == 0). by rewrite (eqP Hlam') !mul0r eqxx in Hn0. move/leq_sizeP/(_ #|s|.-1): Hmax. case Hdeg: (maxdeg <= _)%nat. by move/(_ erefl)/eqP; rewrite Hlam'. rewrite leqNgt. move=> _; move: Hdeg. case: #|s| => [|n]. by rewrite ltn0. by rewrite ltnS /= => ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner