proposition: Lemma step_edom_ok : step_edom = start_port |: edom c.
proof: Proof. apply/setP => x. rewrite !inE step_ports_ok /step_nodes Htriv Hcond /= !inE. case: eqP => // -> /=. move/andP: Hcond => [Hsc Hec]. by apply (subsetP (border_p (nodes c)) start_port). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner