proposition: Lemma connected_step_ep x : known_port c' x -> known_port c x -> exists p b1, path (graph_rel c') (x, b1) p && (last (x, b1) p == (inr ep, false)).
proof: Proof. move=> Hx Hx'. move/andP: (Hcond) => [Hsp _]. case: (@Hc x (inl sp)) => //. by apply (subsetP (border_p _)). move=> p [b1 [b2 /andP [Hp Hl]]]. destruct b2. exists (rcons p (inr ep, false)); exists b1. rewrite rcons_path last_rcons (eqP Hl) eqxx. rewrite /= step_edges_sp_ep eqxx sp_in_step_edom !andbT. by apply (sub_path monotonic_step_rel). case: (lastP p) Hp Hl => /=. move=> _ /eqP [] -> _. exists [:: (inr ep, false)]; exists true. by rewrite eqxx /= sp_in_step_edom step_edges_sp_ep eqxx. move=> {}p x' Hp Hl. rewrite last_rcons in Hl. exfalso; move: Hp. rewrite (eqP Hl) rcons_path /graph_rel => /andP [_] /=. case: (last (x,b1) p) => [] [|] a b. by destruct b. case: b => //. rewrite /step_start_cond in Hsp. by rewrite inE Hsp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner