proposition: Lemma tsorted_setU1_l x a l (b : pred T := [predD1 a & x]) : x \notin l -> TS[a, l] -> TS[b, l].
proof: Proof. move=> xNIl [lSa Cl Bl]; apply: tsortedE => /= [|t z tIl tCz]. apply/subsetP=> i; rewrite !inE. by case: eqP => //= [-> /(negP xNIl)//|_ /(subsetP lSa)]. have tC'z : t -[a]-> z. apply: sub_connect_to tCz. by apply/subsetP => i /andP[]. have zIl := Cl _ _ tIl tC'z. have tBz := Bl _ _ tIl tC'z. split => //; suff->: C[t]_(b, l) = C[t]_(a, l) by []. congr nth; apply: eq_in_find => y /= yIl. have [xIa|xNIa] := boolP (x \in a); last first. apply: eq_symconnect_to => x1. by rewrite /b inE /=; case: eqP xNIa => [->/negPf->|]. apply/idP/idP => /=. apply/sub_symconnect_to/subsetP=> u. by rewrite !inE => /andP[]. case/andP=> tCy Cyt. have /eq_symconnect-> : relto b r =2 relto (predC1 x) (relto a r). by move=> x1 y1; rewrite /b /= !inE !andbA. by apply/andP; split; apply: connect_to_C1l => //; apply: contra xNIl=> /Cl->. Qed.
imports: mathcomp(all_ssreflect) extra