The order of $a$ modulo a prime $p$ divides $p-1$

This is Problem 4.114 of N. B. Alfutova and A. V. Ustinov, Algebra and Number Theory (MCCME, 2002), Chapter 4, §4 “Theorems of Fermat and Euler”.

Let $p$ be a prime and let $a$ be an integer not divisible by $p$. Let $k$ be the least positive integer such that

(the multiplicative order of $a$ modulo $p$).

Theorem. Under these assumptions,

This is the basic link between Fermat's little theorem and the orders of residues modulo a prime; it is the starting point of the theory of primitive roots.

Formalization Note The minimality of $k$ is expressed by IsLeast {j : ℕ | 0 < j ∧ a ^ j ≡ 1 [ZMOD p]} k: the number $k$ is a positive exponent with $a^k\equiv 1 \pmod p$, and every positive exponent $j$ with $a^j\equiv1\pmod p$ satisfies $k\le j$.