proposition: Lemma class_acyclicP c (C := [set x in c]) : c \in scc_seq g -> reflect (#|C| <= 1 /\ {in C, forall x, ~~ g x x}) (class_acyclic c).
proof: Proof. case: c => [|v [|w vs]]//= in C * => vsscc. - by have /and3P[_ _] := sccs_partition g; rewrite (sccsP vsscc). - have -> : C = [set v] by apply/setP => x; rewrite !inE. rewrite cards1; apply: (iffP idP) => [Ngvv|[_ /(_ v (set11 _))//]]. by split=> // x; rewrite !inE => /eqP->. have -> : C = v |: (w |: [set x in vs]) by apply/setP => x; rewrite !inE. have := uniq_flatten; rewrite (perm_uniq (perm_flatten (perm_to_rem vsscc))). rewrite /= !inE !mem_cat/= !negb_or -!andbA => /and5P[Nvw vNvs _ wNvs _]. rewrite !cardsU1 !inE (negPf Nvw)/= vNvs wNvs !add1n !ltnS ltn0. by apply: (iffP idP) => // -[]. Qed.
imports: mathcomp(all_ssreflect) extra