proposition: Lemma sccs_acyclicE : sccs_acyclic = acyclic g.
proof: Proof. apply: (sameP allP); apply: (equivP acyclicP); rewrite -(rwP preacyclic_sccsP). split=> /= [[/= Ng scc_le1 c cscc]|acyP]. by apply/class_acyclicP => //; rewrite scc_le1 ?sccsP//; split. split=> [x|C /sccs_ex[c -> /acyP/class_acyclicP[]]//]. have /flattenP[c /[swap] xc cscc] := all_in_flatten x. by have /class_acyclicP[//|_->//] := acyP _ cscc; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) extra