proposition: Lemma card_ports_nodes_start i : start_dist i != 0 -> (#|ports (nodes (start_graph i))| <= maxdeg)%nat.
proof: Proof. rewrite /= /ports big_set1. rewrite /start_dist. case: ifP => Hi0; try by rewrite eqxx. rewrite mulf_eq0 => Hi. move: (@max_card port (mem i)); rewrite -bin_gt0. rewrite -(ltr0n K) -invr_gt0 lt_def => /andP [HC _]. rewrite (negbTE HC) orbF in Hi. move/leq_sizeP/(_ #|i|.-1): (leq_maxl (size lam) (size rho)). rewrite -/maxdeg. case Hdeg: (maxdeg <= _)%nat. by move/(_ erefl)/eqP => Hi'; rewrite Hi' in Hi. rewrite leqNgt. move=> _; move: Hdeg. case: #|i| => [|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