proposition: Lemma connected_step_out x y : known_port c' x -> known_port c' y -> known_port c x -> known_port c y = false -> connected_ports c' x y.
proof: Proof. move=> Hx Hy Hx' Hy'. move: (connected_step_ep Hx Hx') => [p [b1 Hep]]. move: Hy; rewrite known_port_step // Hy' orbF => /imsetP [y' Hy'en Hyy']. case Hyep: (y == inr ep). rewrite (eqP Hyep). by exists p; exists b1; exists false. case Hen: (en \in conodes c). move: Hy'. rewrite Hyy' /= /ports => /bigcupP. by elim; exists en. exists (rcons p (y,true)); exists b1; exists true. rewrite rcons_path last_rcons eqxx. move/andP: Hep => [] -> /eqP -> /=. rewrite Hyy' andbT. apply/existsP; exists en. case: eqP => Hepy' /=. by rewrite Hepy' Hyy' eqxx in Hyep. by rewrite Hy'en en_in_step_conodes ep_in_en. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner