proposition: Lemma tsorted_cat a l1 l2 : TS[a, l1] -> TS[[predD a & [pred x in l1]], l2] -> TS[a, l2 ++ l1].
proof: Proof. set b := [predD _ & _]. move=> [l1Sa Cl1 Bl1] [l2Sb Cl2] Bl2. apply: tsortedE => [|x y]. apply/subsetP => z. rewrite mem_cat => /orP[/(subsetP l2Sb)|/(subsetP l1Sa) //]. by rewrite inE => /andP[]. have [xIl2 _ Hc|xNIl2] := boolP (x \in l2); last first. rewrite mem_cat (negPf xNIl2) /= => xIl1 Cxy. have yIl1 := Cl1 _ _ xIl1 Cxy. have xBy := Bl1 _ _ xIl1 Cxy. split; first by rewrite mem_cat yIl1 orbT. rewrite /before [index y _]index_cat. have [yIl2|yNil2] := boolP (y \in l2). have/subsetP/(_ y yIl2)/= := l2Sb. by rewrite !inE /= yIl1. rewrite index_cat; have [rIl2| rNIl2] := boolP (_ \in l2). by apply: leq_trans (index_size _ _) (leq_addr _ _). rewrite leq_add2l. move: rNIl2; rewrite /can_to find_cat. have [HH|HH] := boolP (has _ _). by rewrite nth_cat -has_find HH mem_nth // -has_find. rewrite nth_cat ltnNge leq_addr /= => _. by rewrite addnC addnK. have [/forallP F|] := boolP [forall z, [&& z != x, x -[a]-> z & z -[a]-> y] ==> (z \notin l1)]. have xCy : x -[b]-> y. have /eq_connect-> : relto [predD a & [pred x in l1]] r =2 relto [predC [pred x in l1]] (relto a r). by move=> x1 y1; rewrite /= !inE !andbA. apply: connect_to_forced => // z zDx xCz zCy. rewrite !inE /=. have /implyP->// := F z. by rewrite zDx xCz. have yIl2 := Cl2 _ _ xIl2 xCy. have xBy := Bl2 _ _ xIl2 xCy. split; first by rewrite mem_cat yIl2. rewrite /before [index y _]index_cat yIl2. apply: leq_trans xBy. rewrite can_to_cat // index_cat mem_can_to //. apply: before_can_toW=> //; apply/subsetP=> i. by rewrite !inE => /andP[]. rewrite negb_forall => /existsP[z]. rewrite negb_imply -!andbA negbK => /and4P[zDx xCz zCy zIl1]. have yIl1 := Cl1 _ _ zIl1 zCy. have zBy := Bl1 _ _ zIl1 zCy. split; first by rewrite mem_cat yIl1 orbT. rewrite /before [index y _]index_cat. have [yIl2|_] := boolP (_ \in _). have/subsetP/(_ y yIl2)/= := l2Sb. by rewrite !inE yIl1. rewrite index_cat. have [_|/negP[]] := boolP (_ \in _). by apply: leq_trans (index_size _ _) (leq_addr _ _). rewrite /can_to; elim: (l2) xIl2 => //= a1 l IH. rewrite inE => /orP[/eqP->|/IH]; first by rewrite symconnect0 inE eqxx. case: (_ =[_]= _) => //=; first by rewrite inE eqxx. by rewrite inE orbC => ->. Qed.
imports: mathcomp(all_ssreflect) extra