proposition: Lemma cycle_ex_symconnect g x p : cycle g (x :: p) -> ~~ g x x -> exists2 y, x != y & symconnect g x y.
proof: Proof. case: p => [/andP[->]//|y p] /[dup] /symconnect_cycle/(_ x y) sg /andP[gxy _]. by exists y; rewrite ?sg ?(in_cons, eqxx, orbT)//; apply: contraTneq gxy => <-. Qed.
imports: mathcomp(all_ssreflect) extra