proposition: Lemma eq_preacyclic : {homo preacyclic : g g' / connect g =2 connect g' >-> g = g'}.
proof: Proof. by move=> g g' eqg; apply/idP/idP; apply/sub_preacyclic => x y; rewrite (eqg, =^~eqg); apply: connect1. Qed.
imports: mathcomp(all_ssreflect) extra