proposition: Lemma step_edges_inj : {in step_edom &, injective step_edges}.
proof: Proof. rewrite /step_edges. case: ifP => [/andP [Htriv Hcond]|Hcond] x y Hx Hy. + rewrite !ffunE /=. case: ifPn => Hxs. rewrite (eqP Hxs). case: ifPn => Hys. by rewrite (eqP Hys). move=> Hey. have Hy': y \in edom c by apply step_edom_edom. move/andP: Hcond => [_]. by rewrite /step_end_cond in_setD -edom_codom Hey imset_f. case: ifPn => Hys. move=> Hex. have Hx': x \in edom c by apply step_edom_edom. move/andP: Hcond => [_]. by rewrite /step_end_cond in_setD -edom_codom -Hex imset_f. by move=> Heq; apply (@edges_inj _ c x y); auto using step_edom_edom. rewrite /step_edom /step_nodes Hcond in Hx Hy. by move=> Heq; apply (@edges_inj _ c x y). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner