proposition: Lemma findex_head (T : finType) (x y : T) (s : seq T) (uniq_xs : uniq (x::s)) : findex (next (x :: s)) x y = index y (x :: s).
proof: Proof. rewrite /findex (_ : orbit (next (x::s)) x = x::s) // /orbit. rewrite (@order_cycle _ _ (x::s)) ?mem_head ?cycle_next //. exact: (@traject_next _ x). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)