proposition: Lemma tsortedE a l : l \subset a -> (forall x y, x \in l -> x -[a]-> y -> y \in l /\ C[x]_(a, l) =[l]< y) -> TS[a, l].
proof: Proof. by move=> lSa HR; split => // x y xIl xCy; have [] := HR _ _ xIl xCy. Qed.
imports: mathcomp(all_ssreflect) extra