lean_workbook_plus_30556

import Mathlib.Analysis.Complex.Basic

theorem lean_workbook_plus_30556 (p : ℕ) (k : ℕ) (h₁ : k < 4 * p + 1) (h₂ : k ^ 4 ≡ 1 [ZMOD 4 * p + 1]) : ∃ m : ℕ, k ^ m ≡ 1 [ZMOD 4 * p + 1] ∧ m < 4 * p + 1   :=  by sorry