proposition: Lemma tree_like_step : weighted_count (@tree_like _) next_graphs / weighted_count predT next_graphs = (#|port| - #|known_coports c|)%:R / #|free_coports|%:R.
proof: Proof. rewrite weight_is_dist divr1 /weighted_count big_map big_enum_in /=. rewrite -big_distrl -big_distrr /= mul1r; congr (_ / _). rewrite (bigID (fun ps => ps.1 \in known_coports c)) /=. rewrite big_pred0 ?add0r; last first. move=> /= i; apply/negbTE; rewrite negb_and -implybE. by apply/implyP => /andP[] /step_dest_port /andP[] /tree_like_no_sharing. rewrite -sum_step_out. apply eq_bigl => /= i. rewrite andbAC; apply/andb_idr. move/andP=> [] /step_dest_port /andP[]; by apply no_sharing_tree_like. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner