proposition: Lemma cyclePmin x y : y \in <[x]> -> {i | i < #[x] & y = x ^+ i}.
proof: Proof. rewrite cycle_traject; set tx := traject _ _ #[x] => tx_y; pose i := index y tx. have lt_i_x : i < #[x] by rewrite -index_mem size_traject in tx_y. by exists i; rewrite // [x ^+ i]iteropE /= -(nth_traject _ lt_i_x) nth_index. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)