proposition: Lemma sccs_ex C : C \in sccs g -> exists2 c, C = [set x in c] & c \in scc_seq g.
proof: Proof. move=> /(partition_ex (sccs_partition g))[x ->]. have /flattenP[c cscc xc] := all_in_flatten x; exists c => //. apply/setP=> y; rewrite inE; have [z cz] := class_symconnect cscc. by rewrite mem_scc cz; rewrite cz in xc; apply/esym/left_trans. Qed.
imports: mathcomp(all_ssreflect) extra