proposition: Lemma nth_find_symconnect s x : x \in s -> nth x s (find (symconnect g x) s) = x.
proof: Proof. move=> xs; suff /eq_find-> : symconnect g x =1 pred1 x by rewrite nth_index. by move=> y; rewrite acyclic_symconnect_eq// inE eq_sym. Qed.
imports: mathcomp(all_ssreflect) extra acyclic kosaraju