Theme/Drive.lean — FrcCore

1import FrcCore.Theme.Field23/-!4# FrcCore.Theme.Drive — every prime carries a frame (the foundation theme, task LM23)56The formal shadow of C1 (master A12, the label as of 9 October 2026): every prime shell `𝔽_p` has a primitive root, a drive `g` of order `p − 1`, and7its powers reach every nonzero residue. No generator is assumed anywhere: the proof stands on `Theme/Field.lean`8(Fermat's little theorem, no zero divisors, the root bound of `x^m − 1`) and on the naturals.910The order `n` of a nonzero `x` is the least positive `n` with `xⁿ = 1` (`HasOrder`, found by search below `p`); `xᵏ = 1`11iff `n ∣ k`. For a prime power `qᵉ ∣ p − 1` the root bound gives `a` with `a^{(p−1)/q} ≠ 1`, and `a^{(p−1)/qᵉ}` has12order exactly `qᵉ`, since the divisors of `qᵉ` are the powers of `q`. Orders `m` and `qᵉ` with `q ∤ m` multiply: an13element killed by both `qᵉ` and `m` is `1`. Splitting off the least prime factor, every divisor of `p − 1` is an order,14`p − 1` among them. The pigeonhole then makes the `p − 1` powers of the drive exhaust the nonzero residues. No axioms.15-/1617namespace FRC1819namespace Nat2021/-! ## Divisibility, the least witness, prime factors and prime powers -/2223theorem dvd_trans' {a b c : Nat} : a ∣ b → b ∣ c → a ∣ c24  | ⟨d, hd⟩, ⟨e, he⟩ => ⟨d * e, by rw [he, hd, FRC.Nat.mul_assoc]⟩2526theorem pos_of_dvd {a b : Nat} (hb : 0 < b) : a ∣ b → 0 < a27  | ⟨d, hd⟩ => Nat.pos_of_ne_zero (fun h => by rw [h, Nat.zero_mul] at hd; rw [hd] at hb; exact Nat.lt_irrefl 0 hb)2829theorem le_of_dvd' {a b : Nat} (hb : 0 < b) : a ∣ b → a ≤ b30  | ⟨d, hd⟩ => by31    have hd0 : 0 < d := Nat.pos_of_ne_zero (fun h => by rw [h, Nat.mul_zero] at hd; rw [hd] at hb; exact Nat.lt_irrefl 0 hb)32    rw [hd]; exact Nat.le_mul_of_pos_right a hd03334theorem eq_one_of_mul_eq_one {n c : Nat} (h : n * c = 1) : n = 1 :=35  Nat.le_antisymm (le_of_dvd' (Nat.zero_lt_succ 0) ⟨c, h.symm⟩)36    (pos_of_dvd (Nat.zero_lt_succ 0) ⟨c, h.symm⟩)3738/-- The least witness below a bound: if some `m < N` has `P m`, a least one does. -/39theorem exists_least (P : Nat → Prop) [DecidablePred P] :40    ∀ N, (∃ m, m < N ∧ P m) → ∃ m, m < N ∧ P m ∧ ∀ l, l < m → ¬ P l41  | 0, ⟨m, hm, _⟩ => absurd hm (Nat.not_lt_zero m)42  | N + 1, h =>43    match FRC.Shell.decExistsLT P N with44    | .isTrue h' => match exists_least P N h' with45      | ⟨m, hm, hP, hl⟩ => ⟨m, Nat.lt_succ_of_lt hm, hP, hl⟩46    | .isFalse hno => match h with47      | ⟨m, hm, hP⟩ => ⟨m, hm, hP, fun l hl hPl => hno ⟨l, Nat.lt_of_lt_of_le hl (Nat.le_of_lt_succ hm), hPl⟩⟩4849/-- Every `n ≥ 2` has a prime divisor: its least divisor `d ≥ 2`. -/50theorem exists_prime_dvd {n : Nat} (hn : 2 ≤ n) : ∃ q, isPrime q ∧ q ∣ n := by51  have hn0 : 0 < n := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hn52  obtain ⟨d, _, ⟨hd2, hdn⟩, hmin⟩ := exists_least (fun d => 2 ≤ d ∧ n % d = 0) (n + 1)53    ⟨n, Nat.lt_succ_self n, hn, FRC.Nat.mod_self n hn0⟩54  have hd0 : 0 < d := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hd255  have hdvd : d ∣ n := (dvd_iff_mod hd0).2 hdn56  refine ⟨d, ⟨hd2, fun e hed he2 hde => hmin e hed ⟨he2, ?_⟩⟩, hdvd⟩57  have he0 : 0 < e := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) he258  exact (dvd_iff_mod he0).1 (dvd_trans' ((dvd_iff_mod he0).2 hde) hdvd)5960/-- The `q`-part: every `n > 0` is `qᵉ · m` with `q ∤ m`. -/61theorem exists_pow_mul {q : Nat} (hq : 2 ≤ q) : ∀ B n, n ≤ B → 0 < n → ∃ e m, n = q ^ e * m ∧ m % q ≠ 062  | 0, n, hB, hn => absurd (Nat.lt_of_lt_of_le hn hB) (Nat.lt_irrefl 0)63  | B + 1, n, hB, hn => by64    have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq65    match Nat.decEq (n % q) 0 with66    | .isFalse h => exact ⟨0, n, by rw [Nat.pow_zero, Nat.one_mul], h⟩67    | .isTrue h =>68      obtain ⟨c, hc⟩ := FRC.Nat.mod_spec q hq0 n69      rw [h, Nat.add_zero] at hc70      have hc0 : 0 < c := Nat.pos_of_ne_zero (fun e => by rw [e, Nat.mul_zero] at hc; rw [hc] at hn; exact Nat.lt_irrefl 0 hn)71      have hcn : c < n := by72        rw [hc]73        calc c = 1 * c := (Nat.one_mul c).symm74          _ < q * c := FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) hq) hc075      obtain ⟨e, m, hem, hm⟩ := exists_pow_mul hq B c (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hcn hB)) hc076      refine ⟨e + 1, m, ?_, hm⟩77      rw [hc, hem, Nat.pow_succ, Nat.mul_comm (q ^ e) q, FRC.Nat.mul_assoc]7879/-- The divisors of a prime power are the powers: `n ∣ qᵉ` gives `n = qʲ` with `j ≤ e`. -/80theorem dvd_prime_pow {q : Nat} (hq : isPrime q) : ∀ e n, n ∣ q ^ e → ∃ j, j ≤ e ∧ n = q ^ j81  | 0, n, ⟨c, hc⟩ => ⟨0, Nat.le_refl 0, eq_one_of_mul_eq_one (by rw [← hc]; rfl)⟩82  | e + 1, n, ⟨c, hc⟩ => by83    have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq.184    have hqe : q ^ (e + 1) = q * q ^ e := by rw [Nat.pow_succ, Nat.mul_comm]85    match Nat.decEq (n % q) 0 with86    | .isTrue hn =>87      obtain ⟨n', hn'⟩ := FRC.Nat.mod_spec q hq0 n88      rw [hn, Nat.add_zero] at hn'89      have e1 : q * q ^ e = q * (n' * c) := by rw [← hqe, hc, hn', FRC.Nat.mul_assoc]90      obtain ⟨j, hj, hj'⟩ := dvd_prime_pow hq e n' ⟨c, Nat.eq_of_mul_eq_mul_left hq0 e1⟩91      exact ⟨j + 1, Nat.succ_le_succ hj, by rw [hn', hj', Nat.pow_succ, Nat.mul_comm]⟩92    | .isFalse hn =>93      have hnc : (n * c) % q = 0 := by94        rw [← hc, hqe]; exact FRC.Nat.mul_mod_eq_zero_left hq0 (FRC.Nat.mod_self q hq0)95      have hcq : c % q = 0 := match prime_mul_mod hq hnc with96        | .inl h => absurd h hn97        | .inr h => h98      obtain ⟨c', hc'⟩ := FRC.Nat.mod_spec q hq0 c99      rw [hcq, Nat.add_zero] at hc'100      have e1 : q * q ^ e = q * (n * c') := by101        rw [← hqe, hc, hc', FRC.Nat.mul_left_comm]102      obtain ⟨j, hj, hj'⟩ := dvd_prime_pow hq e n ⟨c', Nat.eq_of_mul_eq_mul_left hq0 e1⟩103      exact ⟨j, Nat.le_succ_of_le hj, hj'⟩104105end Nat106107namespace Shell108namespace Prime109110variable {p : Nat} [Pos p]111112/-! ## The order of a nonzero residue -/113114/-- `x` has order `n`: `0 < n`, `xⁿ = 1`, and no positive power below `n` is `1`. -/115def HasOrder (x : Shell p) (n : Nat) : Prop := 0 < n ∧ x ^ n = 1 ∧ ∀ l, l < n → 0 < l → x ^ l ≠ 1116117theorem pow_ne_zero (hp : FRC.Nat.isPrime p) {x : Shell p} (hx : x ≠ 0) : ∀ k : Nat, x ^ k ≠ 0118  | 0 => one_ne_zero hp119  | k + 1 => mul_ne_zero hp (pow_ne_zero hp hx k) hx120121/-- Every nonzero residue has an order below `p` (the least positive exponent with `xⁿ = 1`; Fermat bounds it). -/122theorem exists_order (hp : FRC.Nat.isPrime p) {x : Shell p} (hx : x ≠ 0) : ∃ n, n < p ∧ HasOrder x n := by123  have hp1 : 0 < p - 1 := by124    match p, hp.1 with125    | k + 2, _ => exact Nat.zero_lt_succ k126  obtain ⟨n, hn, ⟨hn0, hxn⟩, hmin⟩ := FRC.Nat.exists_least (fun l => 0 < l ∧ x ^ l = 1) p127    ⟨p - 1, Nat.sub_lt Pos.pos (Nat.zero_lt_succ 0), hp1, fermat hp hx⟩128  exact ⟨n, hn, hn0, hxn, fun l hl hl0 hxl => hmin l hl ⟨hl0, hxl⟩⟩129130theorem pow_eq_one_of_dvd {x : Shell p} {n k : Nat} (h : HasOrder x n) : n ∣ k → x ^ k = 1131  | ⟨c, hc⟩ => by rw [hc, pow_mul, h.2.1, one_pow]132133theorem dvd_of_pow_eq_one {x : Shell p} {n k : Nat} (h : HasOrder x n) (hk : x ^ k = 1) : n ∣ k := by134  obtain ⟨c, hc⟩ := FRC.Nat.mod_spec n h.1 k135  rw [hc, pow_add, pow_mul, h.2.1, one_pow, one_mul] at hk136  match Nat.decEq (k % n) 0 with137  | .isTrue h0 => exact ⟨c, by rw [h0, Nat.add_zero] at hc; exact hc⟩138  | .isFalse h0 => exact absurd hk (h.2.2 _ (Nat.mod_lt k h.1) (Nat.pos_of_ne_zero h0))139140/-- A nonzero `w` with `w^{qᵉ} = 1` and `w^m = 1`, `q` prime and `q ∤ m`, is `1`: its order divides `qᵉ`, so it is a141power of `q`, and it divides `m`, so it is `q⁰`. -/142theorem eq_one_of_pows (hp : FRC.Nat.isPrime p) {q e m : Nat} (hq : FRC.Nat.isPrime q) {w : Shell p} (hw : w ≠ 0)143    (he : w ^ (q ^ e) = 1) (hm : w ^ m = 1) (hmq : m % q ≠ 0) : w = 1 := by144  obtain ⟨n, _, hn⟩ := exists_order hp hw145  obtain ⟨j, _, hj⟩ := FRC.Nat.dvd_prime_pow hq e n (dvd_of_pow_eq_one hn he)146  have hnm := dvd_of_pow_eq_one hn hm147  match j, hj with148  | 0, hj => rw [hj, Nat.pow_zero] at hn; have := hn.2.1; rwa [pow_one] at this149  | j + 1, hj =>150    have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq.1151    have hqn : q ∣ n := ⟨q ^ j, by rw [hj, Nat.pow_succ, Nat.mul_comm]⟩152    exact absurd ((FRC.Nat.dvd_iff_mod hq0).1 (FRC.Nat.dvd_trans' hqn hnm)) hmq153154/-- Orders `m` and `qᵉ` with `q ∤ m` multiply: `y z` has order `m qᵉ`. -/155theorem hasOrder_mul (hp : FRC.Nat.isPrime p) {q e m : Nat} (hq : FRC.Nat.isPrime q) {y z : Shell p}156    (hy0 : y ≠ 0) (hz0 : z ≠ 0) (hy : HasOrder y m) (hz : HasOrder z (q ^ e)) (hmq : m % q ≠ 0) :157    HasOrder (y * z) (m * q ^ e) := by158  refine ⟨Nat.mul_pos hy.1 hz.1, ?_, fun l hl hl0 hyz => ?_⟩159  · rw [mul_pow, pow_mul, hy.2.1, one_pow, one_mul, Nat.mul_comm, pow_mul, hz.2.1, one_pow]160  · rw [mul_pow] at hyz161    have hzl : z ^ l = 1 := by162      refine eq_one_of_pows hp hq (pow_ne_zero hp hz0 l) (by rw [pow_mul_comm, hz.2.1, one_pow]) ?_ hmq163      have h1 : (y ^ l * z ^ l) ^ m = 1 := by rw [hyz, one_pow]164      rwa [mul_pow, pow_mul_comm, hy.2.1, one_pow, one_mul] at h1165    have hyl : y ^ l = 1 := by rw [hzl, mul_one] at hyz; exact hyz166    obtain ⟨l', hl'⟩ := dvd_of_pow_eq_one hz hzl167    have hyl' : y ^ l' = 1 := by168      refine eq_one_of_pows hp (e := e) hq (pow_ne_zero hp hy0 l') ?_ (by rw [pow_mul_comm, hy.2.1, one_pow]) hmq169      rw [← pow_mul, Nat.mul_comm, ← hl']; exact hyl170    obtain ⟨c, hc⟩ := dvd_of_pow_eq_one hy hyl'171    have hle : m * q ^ e ≤ l := FRC.Nat.le_of_dvd' hl0172      ⟨c, by rw [hl', hc, Nat.mul_comm m (q ^ e), FRC.Nat.mul_assoc]⟩173    exact absurd hl (Nat.not_lt_of_le hle)174175/-- A prime power `qᵉ ∣ p − 1`, `e ≥ 1`, is an order: with `p − 1 = qᵉ t` and `a^{(p−1)/q} ≠ 1` (the root bound),176`aᵗ` has order `qᵉ`. -/177theorem exists_order_prime_pow (hp : FRC.Nat.isPrime p) {q e : Nat} (hq : FRC.Nat.isPrime q) (he : 0 < e)178    (hdvd : q ^ e ∣ p - 1) : ∃ z : Shell p, z ≠ 0 ∧ HasOrder z (q ^ e) := by179  obtain ⟨t, ht⟩ := hdvd180  have hp1 : 0 < p - 1 := by181    match p, hp.1 with182    | k + 2, _ => exact Nat.zero_lt_succ k183  match e, he with184  | e + 1, _ =>185    have hq2 : 2 ≤ q := hq.1186    have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq2187    have hpd : p - 1 = q * (q ^ e * t) := by rw [ht, Nat.pow_succ, Nat.mul_comm (q ^ e) q, FRC.Nat.mul_assoc]188    have hd0 : 0 < q ^ e * t := Nat.pos_of_ne_zero (fun h => by rw [h, Nat.mul_zero] at hpd; rw [hpd] at hp1; exact Nat.lt_irrefl 0 hp1)189    have hdlt : q ^ e * t < p - 1 := by190      rw [hpd]191      calc q ^ e * t = 1 * (q ^ e * t) := (Nat.one_mul _).symm192        _ < q * (q ^ e * t) := FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) hq2) hd0193    obtain ⟨a, ha0, had⟩ := exists_pow_ne_one hp hd0 hdlt194    have hz0 : a ^ t ≠ 0 := pow_ne_zero hp ha0 t195    have hzq : (a ^ t) ^ (q ^ (e + 1)) = 1 := by rw [← pow_mul, Nat.mul_comm, ← ht, fermat hp ha0]196    obtain ⟨n, _, hn⟩ := exists_order hp hz0197    obtain ⟨j, hj, hjn⟩ := FRC.Nat.dvd_prime_pow hq (e + 1) n (dvd_of_pow_eq_one hn hzq)198    match Nat.lt_or_ge j (e + 1) with199    | .inl hlt =>200      have hje : q ^ j ∣ q ^ e := ⟨q ^ (e - j), by rw [← FRC.Nat.pow_add, FRC.Nat.add_sub_of_le (Nat.le_of_lt_succ hlt)]⟩201      have h1 : (a ^ t) ^ (q ^ e) = 1 := pow_eq_one_of_dvd hn (by rw [hjn]; exact hje)202      rw [← pow_mul, Nat.mul_comm] at h1203      exact absurd h1 had204    | .inr hge =>205      have : j = e + 1 := Nat.le_antisymm hj hge206      rw [this] at hjn207      exact ⟨a ^ t, hz0, hjn ▸ hn⟩208209/-- Every divisor `n` of `p − 1` is an order: `n = qᵉ m` with `q` the least prime factor and `q ∤ m`; `m` is an order210by induction, `qᵉ` by the root bound, and the two multiply. -/211theorem exists_order_of_dvd (hp : FRC.Nat.isPrime p) :212    ∀ B n, n ≤ B → 0 < n → n ∣ p - 1 → ∃ y : Shell p, y ≠ 0 ∧ HasOrder y n213  | 0, n, hB, hn, _ => absurd (Nat.lt_of_lt_of_le hn hB) (Nat.lt_irrefl 0)214  | B + 1, n, hB, hn, hdvd => by215    match n, hn with216    | 1, _ => exact ⟨1, one_ne_zero hp, Nat.zero_lt_succ 0, one_pow 1,217        fun l hl hl0 => absurd (Nat.lt_of_lt_of_le hl0 (Nat.le_of_lt_succ hl)) (Nat.lt_irrefl 0)⟩218    | k + 2, _ =>219      obtain ⟨q, hq, hqn⟩ := FRC.Nat.exists_prime_dvd (Nat.le_add_left 2 k)220      have hq2 : 2 ≤ q := hq.1221      have hq0 : 0 < q := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 1) hq2222      obtain ⟨e, m, hem, hmq⟩ := FRC.Nat.exists_pow_mul hq2 (k + 2) (k + 2) (Nat.le_refl _) (Nat.zero_lt_succ _)223      have hm0 : 0 < m := Nat.pos_of_ne_zero (fun h => by rw [h, Nat.mul_zero] at hem; exact Nat.noConfusion hem)224      have he0 : 0 < e := by225        match e, hem with226        | 0, hem =>227          rw [Nat.pow_zero, Nat.one_mul] at hem228          rw [hem] at hqn229          exact absurd ((FRC.Nat.dvd_iff_mod hq0).1 hqn) hmq230        | e + 1, _ => exact Nat.zero_lt_succ e231      have hqe : 2 ≤ q ^ e := by232        match e, he0 with233        | e + 1, _ =>234          rw [Nat.pow_succ]235          calc 2 ≤ q := hq2236            _ = 1 * q := (Nat.one_mul q).symm237            _ ≤ q ^ e * q := Nat.mul_le_mul_right q (Nat.pos_pow_of_pos e hq0)238      have hmn : m < k + 2 := by239        rw [hem]240        calc m = 1 * m := (Nat.one_mul m).symm241          _ < q ^ e * m := FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) hqe) hm0242      obtain ⟨y, hy0, hy⟩ := exists_order_of_dvd hp B m (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hmn hB)) hm0243        (FRC.Nat.dvd_trans' ⟨q ^ e, by rw [hem, Nat.mul_comm]⟩ hdvd)244      obtain ⟨z, hz0, hz⟩ := exists_order_prime_pow hp hq he0 (FRC.Nat.dvd_trans' ⟨m, hem⟩ hdvd)245      have h := hasOrder_mul hp hq hy0 hz0 hy hz hmq246      rw [Nat.mul_comm, ← hem] at h247      exact ⟨y * z, mul_ne_zero hp hy0 hz0, h⟩248249/-! ## The drive: a primitive root, and its powers exhaust the nonzero residues -/250251/-- A primitive root: `g^{p−1} = 1` and no positive power below `p − 1` is `1`. -/252theorem exists_primitive (hp : FRC.Nat.isPrime p) :253    ∃ g : Shell p, g ≠ 0 ∧ g ^ (p - 1) = 1 ∧ ∀ l, l < p - 1 → 0 < l → g ^ l ≠ 1 := by254  have hp1 : 0 < p - 1 := by255    match p, hp.1 with256    | k + 2, _ => exact Nat.zero_lt_succ k257  obtain ⟨g, hg0, hg⟩ := exists_order_of_dvd hp (p - 1) (p - 1) (Nat.le_refl _) hp1 ⟨1, (Nat.mul_one _).symm⟩258  exact ⟨g, hg0, hg.2.1, hg.2.2⟩259260/-- 26:E10, 26:F10 — the powers `g⁰, …, g^{p−2}` of a primitive root are distinct. -/261theorem primitive_pow_inj (hp : FRC.Nat.isPrime p) {g : Shell p} (hg0 : g ≠ 0) (hg : HasOrder g (p - 1))262    {i j : Nat} (hi : i < p - 1) (hj : j < p - 1) (h : g ^ i = g ^ j) : i = j := by263  have key : ∀ {i j : Nat}, i ≤ j → j < p - 1 → g ^ i = g ^ j → i = j := by264    intro i j hij hj h265    have e1 : g ^ i * g ^ (j - i) = g ^ i * 1 := by rw [← pow_add, FRC.Nat.add_sub_of_le hij, mul_one, h]266    obtain ⟨c, hc⟩ := dvd_of_pow_eq_one hg (mul_left_cancel hp (pow_ne_zero hp hg0 i) e1)267    match c, hc with268    | 0, hc =>269      rw [Nat.mul_zero] at hc270      rw [← FRC.Nat.add_sub_of_le hij, hc, Nat.add_zero]271    | c + 1, hc =>272      have : p - 1 ≤ j - i := by rw [hc]; exact Nat.le_mul_of_pos_right _ (Nat.zero_lt_succ c)273      exact absurd (Nat.lt_of_le_of_lt this (Nat.lt_of_le_of_lt (Nat.sub_le j i) hj)) (Nat.lt_irrefl _)274  exact match Nat.lt_or_ge i j with275    | .inl hlt => key (Nat.le_of_lt hlt) hj h276    | .inr hge => (key hge hi h.symm).symm277278/-- 00:A12, 26:E10, 26:F10 — every prime carries a frame: the prime shell `𝔽_p` has a drive `g`, a primitive root of order `p − 1`, and279its powers `g^m`, `m < p − 1`, reach every nonzero residue (`⟨g⟩ = 𝔽_p^×`, the pigeonhole). -/280theorem exists_drive (hp : FRC.Nat.isPrime p) :281    ∃ g : Shell p, (g ^ (p - 1) = 1 ∧ ∀ l, l < p - 1 → 0 < l → g ^ l ≠ 1) ∧282      ∀ v, v < p → 0 < v → ∃ m, m < p - 1 ∧ (g ^ m).val = v := by283  obtain ⟨g, hg0, hg1, hgl⟩ := exists_primitive hp284  have hp1 : 0 < p - 1 := by285    match p, hp.1 with286    | k + 2, _ => exact Nat.zero_lt_succ k287  have hg : HasOrder g (p - 1) := ⟨hp1, hg1, hgl⟩288  refine ⟨g, ⟨hg1, hgl⟩, fun v hv hv0 => ?_⟩289  have hp' : p = p - 1 + 1 := (FRC.Nat.sub_add_cancel Pos.pos).symm290  have hinj : ∀ i j, i < p - 1 → j < p - 1 → (g ^ i).val = (g ^ j).val → i = j := fun i j hi hj e =>291    primitive_pow_inj hp hg0 hg hi hj (ext e)292  have hb : ∀ e, Pigeonhole.mem e (imageList (fun m => (g ^ m).val) (p - 1)) → 1 ≤ e ∧ e ≤ p - 1 := fun e he =>293    match mem_imageList he with294    | ⟨m, _, hm⟩ =>295      ⟨Nat.pos_of_ne_zero (fun h0 => pow_ne_zero hp hg0 m (ext (by rw [hm, h0]; rfl))),296       by rw [← hm]; exact Nat.le_of_lt_succ (Nat.lt_of_lt_of_le (g ^ m).lt (Nat.le_of_eq hp'))⟩297  exact mem_imageList (Pigeonhole.mem_of_nodup_of_length (p - 1) _ (imageList_nodup hinj (Nat.le_refl _)) hb298    (imageList_length _ _) v hv0 (Nat.le_of_lt_succ (Nat.lt_of_lt_of_le hv (Nat.le_of_eq hp'))))299300end Prime301end Shell302end FRC303