proposition: Lemma tsorted_cons_r x a l (b : pred T := [predD1 a & x]) : (forall y, y \in l -> x -[a]-> y) -> (forall y, r x y -> a y -> y != x -> y \in l) -> a x -> TS[b, l] -> TS[a, x :: l].
proof: Proof. move=> AxC AyIl Ax [/= lSb Cl Bl]; apply: tsortedE => [|y z] /=. apply/subsetP=> y; rewrite inE => /orP[/eqP->//|/(subsetP lSb)]. by rewrite inE=> /andP[]. have F t : t != x -> x -[b]-> t -> t \in l. move=> tDx /connectP[[_ /eqP|v p]] /=; first by rewrite (negPf tDx). rewrite -!andbA /= => /and4P[vDx vIa xRv Pbrvp tLvp]. have/Cl->// : v \in l. by apply: AyIl => //; rewrite inE. by apply/connectP; exists p. rewrite inE. have Hr : relto b r =2 (relto (predC1 x) (relto a r)). by move=> x1 y1; rewrite /= !inE !andbA. have [/eqP-> /= _ xCz|yDx /= yIl yCz] := boolP (y == x). split; last by rewrite /before /= can_to_cons symconnect0 eqxx. have [/eqP<-|zDx] := boolP (z == x); first by rewrite !inE eqxx. rewrite inE (F z) ?orbT // 1?eq_sym // (eq_connect Hr). by rewrite -connect_to_C1_id. have [yCz'|yNCz'] := boolP (y -[b]-> z). have zIxs := Cl _ _ yIl yCz'. have yBz := Bl _ _ yIl yCz'. split; first by rewrite inE zIxs orbT. have [/eqP xEz|xDz] := boolP (x == z). rewrite can_to_cons. suff->: y =[a]= x by rewrite /before /= eqxx. rewrite /symconnect {1}xEz yCz /=. by apply: AxC. rewrite can_to_cons; case: (_ =[_]= _); first by rewrite /before /= eqxx. rewrite /before /= (negPf xDz); case: eqP => //= _. rewrite ltnS. apply: leq_trans yBz => /=. apply: before_can_toW => //; apply/subsetP=> i. by rewrite inE => /andP[]. have [yCx|yNCx] := boolP (y -[a]-> x); last first. case/negP: yNCz'. by rewrite (eq_connect Hr); apply: connect_to_C1l. have [xCz| xNCz] := boolP (x -[a]-> z); last first. case/negP: yNCz'. by rewrite (eq_connect Hr); apply: connect_to_C1r. split. rewrite inE. have [//|zDx/=] := boolP (z == x). apply: F => //. by rewrite (eq_connect Hr) -connect_to_C1_id. rewrite /before can_to_cons. suff->: y =[a]= x; first by rewrite /before /= eqxx. rewrite /symconnect yCx /=. by apply: AxC. Qed.
imports: mathcomp(all_ssreflect) extra