proposition: Lemma preacyclic_eqP {g} : reflect (symconnect g =2 eq_op) (preacyclic g).
proof: Proof. apply: (iffP preacyclicP); last by move=> eqg x y; rewrite eqg => /eqP. by move=> eqxy x y; apply/idP/eqP => [/eqxy//|->]. Qed.
imports: mathcomp(all_ssreflect) extra