proposition: Theorem tree_like_neighbor : (weighted_count (@tree_like _ \o snd) next_graphs / weighted_count predT next_graphs) >= ((#|port| - maxdeg * tree_max l.+1)%:R / #|port|%:R) ^+ (maxdeg * tree_max l).
proof: Proof. rewrite 2!weighted_count_next. have Hlam : (size lam <= maxdeg)%nat by apply leq_maxl. have Hrho : (size rho <= maxdeg)%nat by apply leq_maxr. have Hw := weighted_count_start_is_dist Hlam Hrho. rewrite weighted_count_next in Hw. clear next_graphs. apply le_sum_all. - by rewrite /= Hw ltr01. - move=> i. case: ifP => // Hi _. rewrite (@weighted_count_switch_it maxdeg def_port maxdeg) //. + rewrite lt_def Hi /=; exact: start_dist_ge0. + by rewrite card_ports_nodes_start // Hi. + by rewrite /known_coports /ports /= big_set0 cards0. - move=> /= i. case: ifP => Hi // _. apply tree_like_after => //. + by apply connected_start. + by apply tree_like_start. + by rewrite card_ports_nodes_start // Hi. + by rewrite /known_coports /ports /= big_set0 cards0. + rewrite lt_def Hi /=; exact: start_dist_ge0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner