proposition: Lemma cycleV x : <[x^-1]> = <[x]>.
proof: Proof. by apply/eqP; rewrite eq_sym eqEsubset !cycle_subG groupV -groupV !cycle_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)