proposition: Lemma step_dest_port i : i \in dest_port -> trivIset (i.2 |: conodes c) && step_cond c p i.1 i.2.
proof: Proof. rewrite /dest_port inE /free_coports inE andbA => /andP [Hif Htriv]. by rewrite Htriv /step_cond /step_start_cond /step_end_cond Hpb inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner