proposition: Lemma tsorted_connect_before_nth x y : connect g x y -> before vs (nth x vs (find (symconnect g x) vs)) y.
proof: Proof. by move: (vs_all x); apply vs_tsorted. Qed.
imports: mathcomp(all_ssreflect) extra acyclic kosaraju