proposition: Lemma eq_edom_edges_inout x y : let c' := step c p i.1 i.2 in y \in known_coports c -> (x \in edom c') && (edges c' x == y) = (x \in edom c) && (edges c x == y).
proof: Proof. move=> /= Hky. rewrite /edom /= step_edom_ok // 2!inE. case Hx: (x \in edom c) => /=. by rewrite orbT monotonic_edges_step. case Hxp: (x == p) => //=. rewrite (eqP Hxp). rewrite step_edges_sp_ep //. apply/negP => /eqP Hy. by move: Hi1; rewrite Hy Hky. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner