proposition: Lemma tree_like_no_sharing : tree_like (step c p i.1 i.2) -> i.1 \notin known_coports c.
proof: Proof. move=> Htl; apply/negP=> Hi. have Hksp : known_port c (inl p) := subsetP (border_p _) _ Hpb. move: (@Hpc (inl p) (inr i.1) Hksp Hi) => [pa [b1 [b2 /andP [Hp Hl]]]]. move: (last (inl p, b1) pa) Hl (shortenP Hp) => ep /eqP Hep Hsp. destruct Hsp as [p' Hp' Hun _]. have Hb1: b1 = false. case: b1 Hep Hp' {Hp Hun} => //. case: p' => [] // [[|] a [|] l] //=. by rewrite !inE Hpb. subst b1. have Hb2: b2 = true. case: b2 Hep (flip_seq_path Hp') => // Hep. rewrite last_map Hep. case: p' Hep {Hun Hp'} => //= a l. rewrite rev_cons. case: (rev _) => [] // [[|] b [|] l'] //=. case Hbdom: (b \in _) => //=. case Hedge: (edges c b == _) => //=. move/andP: Hsc => [Hsp]. rewrite /step_end_cond inE. move/(imset_f (edges c)): Hbdom. by rewrite edom_codom (eqP Hedge) => ->. subst b2. have Hlen: (size p' < #|port|*4)%nat. move: (@uniq_leq_size _ _ (enum [set: graph_node port * bool]) Hun). rewrite -cardE cardsT /=. rewrite card_prod card_bool card_sum addnn -muln2 -mulnA. apply => x _. by rewrite mem_enum inE. move: Htl. rewrite /tree_like => /forallP/(_ (Ordinal Hlen)). have Hlen': size ((inl p, false)::p') = (Ordinal Hlen).+1 by []. move/forallP/(_ (tcast Hlen' (in_tuple ((inl p, false)::p')))). move/negP; apply. rewrite /ucycleb /= /path.cycle /=. rewrite eq_tcast [X in X && _]/=. rewrite rcons_path Hun andbT /=. rewrite (sub_path (monotonic_step_rel p i.1 i.2) Hp') Hep /=. by rewrite sp_in_step_edom // step_edges_sp_ep // eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner