proposition: Lemma monotonic_edges_step x : x \in edom c -> edges c' x = edges c x.
proof: Proof. move=> Hx. case Hcond: (step_trivIset c en && step_cond c sp ep en). move/andP: Hcond => [Htriv Hcond]. rewrite step_edges_ok //. case: ifP => // Hxsp. move/andP: Hcond => []. rewrite /step_start_cond => Hsp. by rewrite /edom /graph_dom inE (eqP Hxsp) Hsp in Hx. by rewrite /= step_edges_id. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner