proposition: Lemma preacyclic_connect : {homo connect : g / preacyclic g}.
proof: Proof. move=> g /preacyclic_eqP eqsc; apply/preacyclicP => x y. by rewrite symconnect_connect eqsc => /eqP. Qed.
imports: mathcomp(all_ssreflect) extra