proposition: Lemma acyclic_cycleP {g} : reflect (forall p, ~~ nilp p -> sorted g p -> ~~ cycle g p) (acyclic g).
proof: Proof. apply: (iffP acyclicP) => [|Ncycle]; last first. split; first by move=> x; have /(_ _ _)/nandP[] := Ncycle [:: x]. apply/preacyclicP => x y; apply: contraTeq => neqxy. apply/symconnect_cycle2P => // -[p yp] /[dup]. by rewrite [X in X -> _]/= rcons_path => /andP[gxp _]; apply/negP/Ncycle. move=> [/(_ _)/negPf gN] /preacyclic_eqP e. move=> [//|x [/=|y p] _]; rewrite ?gN// => /andP[gxy _]. have: ~~ symconnect g x y by rewrite e; apply: contraTneq gxy => ->; rewrite gN. by apply: contra => /symconnect_cycle->; rewrite ?(in_cons, eqxx, orbT). Qed.
imports: mathcomp(all_ssreflect) extra