proposition: Lemma no_sharing_tree_like : tree_like (step c p i.1 i.2).
proof: Proof. apply/'forall_forallP => /= n px. apply/negP => /andP [Hcy Hun]. move/negbT: (no_cycle_in_known_ports Hcy Hun). move/allPn => /= [[x b]] /= Hxpx Hxkp. destruct px as [px Hpx]; simpl in *; clear Hpx. wlog: b px Hxpx Hcy Hun / b == false. move=> Hfalse. destruct b; last first. by apply (Hfalse false px). apply (Hfalse false (map (@flip _) (rev px))) => {Hfalse} //. + rewrite -mem_rev in Hxpx. by apply (map_f (@flip _) Hxpx). + destruct px => //=. rewrite -(rotr_cycle 1) -map_rotr. rewrite rev_cons rotr1_rcons /=. move/flip_seq_path: Hcy => /=. by rewrite map_rcons last_rcons belast_rcons map_rev rev_cons map_rev. + rewrite map_rev rev_uniq map_inj_uniq /flip //. move=> [a a'] [b b'] /= [] ->. by move/negb_inj => ->. move/eqP => Hb; subst b. move: (next_cycle Hcy Hxpx). move/graph_rel_known_port => /= [[Hkpx Hkpnx] [Hxnx Hbx]]. rewrite !known_port_step // in Hkpx Hkpnx. move/orP: Hkpx => [] Hkpx; last by rewrite Hkpx in Hxkp. move/imsetP: Hkpx => [x' Hx Hxx']. subst x; rename x' into x. case_eq (next px (inr x, false)) => x' b'' Hnx. rewrite Hnx /= in Hxnx Hbx Hkpnx Hxkp. subst b''. move/orP: Hkpnx => [] Hkpnx; last first. move: (next_cycle Hcy Hxpx) => /=. rewrite Hnx. destruct x' as [x'|x'] => //. move/existsP => [s]. case/and4P. rewrite /step_conodes. destruct Bool.bool_dec => //. rewrite Hsc /= !inE => /orP [/eqP -> | Hsco] Hxs Hx's. rewrite /= in Hkpnx. have Hi2p := (trivIset_I1 Htriv Hx's Hkpnx). elim (negP Hxkp). by apply/bigcupP; exists i.2. elim: (negP Hxkp). by apply/bigcupP; exists s. move/imsetP: Hkpnx => [x'' Hx' Hxx']. subst x'; rename x'' into x'. have Hix': x' = i.1. rewrite -mem_next Hnx in Hxpx. move: (next_cycle Hcy Hxpx). case_eq (next px (inr x', true)) => /= x'' b'' Hx''. rewrite Hx''. destruct x'' as [x''|x''] => //. destruct b'' => //. move/andP => [Hex'']. rewrite /step_edges /= /step_trivIset Htriv Hsc /= ffunE /=. case: ifP => Hx''p. by rewrite eq_sym => /eqP. move: (step_edom_edom Htriv Hsc (negbT Hx''p) Hex'') => Hx''e Hed. move/setP/(_ x'): (edom_codom c). rewrite -{1}(eqP Hed) imset_f //= => /esym. rewrite !inE => /andP [_] Hx'p. elim (negP Hxkp). apply/bigcupP; exists i.2 => //. by rewrite (trivIset_I1 Htriv Hx'). have Hix: x = i.1. move: (prev_cycle Hcy Hxpx). case_eq (prev px (inr x, false)) => /= x'' b'' Hx''. rewrite Hx''. destruct x'' as [x''|x''], b'' => //=. move/andP => [Hex'']. rewrite /step_edges /= /step_trivIset Htriv Hsc /= ffunE /=. case: ifP => Hx''p. by rewrite eq_sym => /eqP. move: (step_edom_edom Htriv Hsc (negbT Hx''p) Hex'') => Hx''e Hed. move/setP/(_ x): (edom_codom c). rewrite -{1}(eqP Hed) imset_f //= => /esym. rewrite !inE => /andP [_] Hx'p. elim (negP Hxkp). apply/bigcupP; exists i.2 => //. by rewrite (trivIset_I1 Htriv Hx). by rewrite Hix Hix' eqxx in Hxnx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner