proposition: Lemma step_edom_codom : step_edges @: step_edom = graph_dom step_conodes.
proof: Proof. case Hcond: (step_trivIset && step_cond); last first. by rewrite step_conodes_id // step_edom_id // step_edges_id // edom_codom. move/andP: Hcond => [Htriv Hcond]. rewrite step_edom_ok // step_codom_ok //. apply/setP => x. apply/imsetP. case: ifP. - rewrite 2!inE. case Hx: (x == _) => /=. rewrite (eqP Hx). exists start_port. by rewrite !inE eqxx. by rewrite step_edges_ok // eqxx. rewrite -edom_codom => /imsetP [y Hy Hxy]. exists y. by rewrite inE Hy orbT. rewrite Hxy step_edges_ok //. case: ifP => // /eqP Hys. move/andP: Hcond Hy => []. by rewrite inE /step_start_cond -Hys => ->. - move=> Hx [y Hy Hxy]. move/negbT/negP: Hx; elim. move: Hy. rewrite 2!inE Hxy step_edges_ok // => /orP [/eqP ->| Hy]. by rewrite eqxx !inE eqxx /=. case: ifP => Hys. by rewrite !inE eqxx. rewrite inE; apply/orP; right. by rewrite -edom_codom imset_f. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner