proposition: Lemma sub_preacyclic : {homo preacyclic : g g' / subrel g (connect g') >-> g' -> g}.
proof: Proof. move=> g g' subg /preacyclicP eqsc; apply/preacyclicP => x y. by move=> /(sub_symconnect subg)/eqsc. Qed.
imports: mathcomp(all_ssreflect) extra