proposition: Lemma eq_in_porbit s x i j : ((s ^+ i)%g x == (s ^+ j)%g x) = (i == j %[mod #|porbit s x|]).
proof: Proof. Proof using. apply/idP/idP. - rewrite [X in X == _]porbit_mod [X in _ == X]porbit_mod !permX. have HC : 0 < #|porbit s x|. by rewrite card_gt0; apply/set0Pn; exists x. rewrite -!(nth_traject _ (ltn_pmod _ HC)). rewrite nth_uniq // ?size_traject ?ltn_pmod //. exact: uniq_traject_porbit. - by move=> /eqP H; apply/eqP; rewrite [LHS]porbit_mod [RHS]porbit_mod H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp