proposition: Lemma step_edges_out : {in ~: step_edom, step_edges =1 ssrfun.id}.
proof: Proof. move=> p Hp. rewrite /step_edges. case: ifP => Hif. move /andP: Hif => [Htriv Hcond]. move/andP: (Hcond) => [Hsc Hec]. rewrite !ffunE /=. move: Hp. rewrite step_edom_ok //. rewrite 3!inE. case: ifP => _ //= Hp'. by rewrite edges_out // inE. rewrite step_edom_id // in Hp. by rewrite edges_out. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner