proposition: Lemma symconnect_cycle2P g x y : x != y -> reflect (exists2 p, y \in p & cycle g (x :: p)) (symconnect g x y).
proof: Proof. move=> Nxy; apply: (iffP idP) => [|[p yp]]; last first. by move=> /symconnect_cycle->; rewrite ?(in_cons, eqxx, yp, orbT). move: Nxy => /[swap]/andP[/connectP[p gp ->] /connectP[]]. elim/last_ind => /=[_ <-|q z _]; first by rewrite eqxx. rewrite rcons_path last_rcons => /[swap]{z}<- /andP[gq gzq] Nxy. have := mem_last x p; rewrite in_cons eq_sym (negPf Nxy)/= => yp. exists (p ++ q); first by rewrite mem_cat yp. by rewrite rcons_path cat_path gp gq last_cat gzq. Qed.
imports: mathcomp(all_ssreflect) extra