proposition: Lemma preacyclic_sccsP {g} : reflect {in sccs g, forall C : {set V}, #|C| <= 1} (preacyclic g).
proof: Proof. apply: (iffP preacyclicP) => [gNsymc C Cscc | card_sccs_le1 x y]. apply/card_le1_eqP => x y xC yC. by apply: gNsymc; rewrite -mem_scc (def_scc Cscc yC). rewrite -mem_scc => /card_le1_eqP; apply; rewrite ?mem_pblock ?cover_sccs//. by rewrite card_sccs_le1 ?pblock_mem ?cover_sccs. Qed.
imports: mathcomp(all_ssreflect) extra