proposition: Lemma weight_is_dist : weighted_count predT next_graphs = 1.
proof: Proof. rewrite /weighted_count big_map -big_distrl -big_distrr /=. rewrite mul1r /free_coports cardsCp. rewrite (bigID [pred ps | ps.1 \in known_coports c]) /=. rewrite (bigID [pred ps | ps.1 \in border (conodes c)]) /=. rewrite (eq_bigl (fun ps => ps.1 \in border (conodes c))); last first. move=> [x s] /=. case Hb: (x \in border _). rewrite andbT. by move/subsetP: (border_p (conodes c)); apply. by rewrite andbF. rewrite 3!big_enum_in /= sum_step_border sum_step_used addr0 sum_step_out -natrD. rewrite addnBA; last by apply max_card. rewrite addnC. rewrite -subnBA; last by apply card_border_ports. move: free_coports_card. rewrite /free_coports cardsCp. rewrite cardsDS; last by apply border_p. move=> Hf. rewrite divrr // unitfE. apply lt0r_neq0. by rewrite ltr0n. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner