proposition: Lemma enum_step_border c s b x : enum (border (nodes c)) = s :: b -> x \in dest_port c -> enum (border (nodes (step c s x.1 x.2))) = b.
proof: Proof. move=> Heqb Hx. have Hhead: s \in border (nodes c). by rewrite -mem_enum Heqb inE eqxx. rewrite /= /step_nodes /step_trivIset step_dest_port //=. move: (Heqb). rewrite (@enum_cons _ _ s) /=. by move=> [->]. by rewrite Heqb. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner