proposition: Lemma weighted_count_start_is_dist : weighted_count predT next_graphs = 1.
proof: Proof. rewrite weighted_count_next. transitivity (\sum_(pn | start_dist pn != 0) start_dist pn). apply eq_bigr => i Hi. rewrite (@weighted_count_switch_it maxdeg def_port maxdeg) //. by apply card_ports_nodes_start => //; rewrite Hi. by rewrite /known_coports /ports /= big_set0 cards0. transitivity (\sum_pn start_dist pn). rewrite [RHS](bigID (fun pn => start_dist pn == 0)) /=. rewrite [in RHS]big1 ?add0r //. by move=> i /eqP. rewrite partition_big_nodes_arities. rewrite /start_dist. rewrite (bigID (fun j : 'I_#|port|.+1 => j == 0)) /=. rewrite big1 /= ?add0r; last first. move=> i /eqP Hi. rewrite big1 // => j /eqP Hj. case: ifP => //. by rewrite Hj Hi eqxx. transitivity (\sum_(j < #|port|.+1 | j != 0) lam`_j.-1 * \sum_(i : {set port} | #|i| == j) 1 / ('C(#|port|, j))%:R). apply eq_bigr => k Hk. rewrite big_distrr /=. apply eq_bigr => i /eqP -> /=. have -> : (k == O :> nat) = false by apply/negbTE. by rewrite mul1r. transitivity (\sum_(j < #|port|.+1 | j != 0) lam`_j.-1). apply eq_bigr => k Hk. rewrite -[RHS]mulr1. f_equal. rewrite -big_distrl -[RHS](@divff K ('C(#|port|, k))%:R) /=. f_equal. by rewrite -card_draws sumr_const cardsE. apply lt0r_neq0. rewrite ltr0n bin_gt0. by apply (ltn_ord k). have HlamE : (size lam <= #|port|)%nat. apply (leq_trans Hlam). rewrite (leq_trans _ (ltnW Hmaxlen)) //. by rewrite /tree_max sum_expr_S mulnDr muln1 leq_addr. by rewrite sum_lambda_pred. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner