have h_proper_div : k ∈ n.properDivisors := Nat.mem_properDivisors.mpr ⟨h₂, h₃⟩
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1
n k : ℕ
x✝ : 1 ≠ k
h₂ : k ∣ n
h₃ : k < n
h_proper_div : k ∈ n.properDivisors
⊢ (X ^ k - 1) * phi n ∣ X ^ n - 1