[GOAL]
n : ℕ
z : ℂ
⊢ ¬(z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0)
[PROOFSTEP]
rintro ⟨h1, h2⟩
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ False
[PROOFSTEP]
replace h3 : z ^ 3 = 1
[GOAL]
case h3
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
⊢ z ^ 3 = 1
[PROOFSTEP]
linear_combination (1 - z - z ^ 2 - z ^ n) * h1 + (z ^ n - 2) * h2
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False
[PROOFSTEP]
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2 :=
  by
  rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
  have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
  interval_cases n % 3 <;> simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
[PROOFSTEP]
rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2
[PROOFSTEP]
have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : n % 3 < 3
⊢ z ^ (n % 3) = 1 ∨ z ^ (n % 3) = z ∨ z ^ (n % 3) = z ^ 2
[PROOFSTEP]
interval_cases n % 3
[GOAL]
case «0»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 0 < 3
⊢ z ^ 0 = 1 ∨ z ^ 0 = z ∨ z ^ 0 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case «1»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 1 < 3
⊢ z ^ 1 = 1 ∨ z ^ 1 = z ∨ z ^ 1 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case «2»
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
this : 2 < 3
⊢ z ^ 2 = 1 ∨ z ^ 2 = z ∨ z ^ 2 = z ^ 2
[PROOFSTEP]
simp only [this, pow_zero, pow_one, eq_self_iff_true, or_true_iff, true_or_iff]
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
⊢ False
[PROOFSTEP]
have z_ne_zero : z ≠ 0 := fun h => zero_ne_one ((zero_pow zero_lt_three).symm.trans (show (0 : ℂ) ^ 3 = 1 from h ▸ h3))
[GOAL]
case intro
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
z_ne_zero : z ≠ 0
⊢ False
[PROOFSTEP]
rcases key with (key | key | key)
[GOAL]
case intro.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ False
[PROOFSTEP]
exact z_ne_zero (by rwa [key, self_eq_add_left] at h1 )
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = 1
⊢ z = 0
[PROOFSTEP]
rwa [key, self_eq_add_left] at h1 
[GOAL]
case intro.inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False
[PROOFSTEP]
exact one_ne_zero (by rwa [key, self_eq_add_right] at h1 )
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ 1 = 0
[PROOFSTEP]
rwa [key, self_eq_add_right] at h1 
[GOAL]
case intro.inr.inr
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ False
[PROOFSTEP]
exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2 ))
[GOAL]
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z ^ 2
⊢ z ^ ?m.10353 = 0
[PROOFSTEP]
rwa [key, add_self_eq_zero] at h2 
[GOAL]
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
by_cases hn0 : n = 0
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
[PROOFSTEP]
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
[PROOFSTEP]
simp only [trinomial, C_neg, C_1]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n
[PROOFSTEP]
ring
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hp]
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (trinomial 0 1 n (-1) (-1) 1)
[PROOFSTEP]
apply IsUnitTrinomial.irreducible_of_coprime' ⟨0, 1, n, zero_lt_one, hn, -1, -1, 1, rfl⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ ∀ (z : ℂ),
    ¬(↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0 ∧ ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0)
[PROOFSTEP]
rintro z ⟨h1, h2⟩
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ False
[PROOFSTEP]
apply X_pow_sub_X_sub_one_irreducible_aux z
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [trinomial_mirror zero_lt_one hn (-1 : ℤˣ).ne_zero (1 : ℤˣ).ne_zero] at h2 
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h2 : ↑(aeval z) (trinomial 0 (n - 1 + 0) n ↑1 ↑(-1) ↑(-1)) = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
simp_rw [trinomial, aeval_add, aeval_mul, aeval_X_pow, aeval_C, Units.val_neg, Units.val_one, map_neg, map_one] at h1 h2 
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
replace h1 : z ^ n = z + 1 := by linear_combination h1
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : -1 * z ^ 0 + -1 * z ^ 1 + 1 * z ^ n = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
⊢ z ^ n = z + 1
[PROOFSTEP]
linear_combination h1
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h2 : 1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n = 0
h1 : z ^ n = z + 1
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
replace h2 := mul_eq_zero_of_left h2 z
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : (1 * z ^ 0 + -1 * z ^ (n - 1 + 0) + -1 * z ^ n) * z = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [add_mul, add_mul, add_zero, mul_assoc (-1 : ℂ), ← pow_succ', Nat.sub_add_cancel hn.le] at h2 
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * z ^ n + -1 * z ^ n * z = 0
⊢ z ^ ?m.21676 = z + 1 ∧ z ^ ?m.21676 + z ^ 2 = 0
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : ↑(aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
⊢ ℕ
[PROOFSTEP]
rw [h1] at h2 ⊢
[GOAL]
case neg.intro
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 = z + 1 ∧ z + 1 + z ^ 2 = 0
[PROOFSTEP]
exact ⟨rfl, by linear_combination -h2⟩
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1✝ : ↑(aeval z) (↑C ↑(-1) * X ^ 0 + ↑C ↑(-1) * X ^ 1 + ↑C ↑1 * X ^ n) = 0
h2✝ : ↑(aeval z) (mirror (trinomial 0 1 n ↑(-1) ↑(-1) ↑1)) = 0
h1 : z ^ n = z + 1
h2 : 1 * z ^ 0 * z + -1 * (z + 1) + -1 * (z + 1) * z = 0
⊢ z + 1 + z ^ 2 = 0
[PROOFSTEP]
linear_combination -h2
[GOAL]
n : ℕ
hn1 : n ≠ 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
by_cases hn0 : n = 0
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]
[GOAL]
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
[PROOFSTEP]
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hp : (X ^ n - X - 1 : ℤ[X]) = trinomial 0 1 n (-1) (-1) 1 := by simp only [trinomial, C_neg, C_1]; ring
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
[PROOFSTEP]
simp only [trinomial, C_neg, C_1]
[GOAL]
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
⊢ X ^ n - X - 1 = -1 * X ^ 0 + -1 * X ^ 1 + 1 * X ^ n
[PROOFSTEP]
ring
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have hn : 1 < n := Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨hn0, hn1⟩
[GOAL]
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
have h := (IsPrimitive.Int.irreducible_iff_irreducible_map_cast ?_).mp (X_pow_sub_X_sub_one_irreducible hn1)
[GOAL]
case neg.refine_2
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
h : Irreducible (map (Int.castRingHom ℚ) (X ^ n - X - 1))
⊢ Irreducible (X ^ n - X - 1)
[PROOFSTEP]
rwa [Polynomial.map_sub, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one, Polynomial.map_X] at h 
[GOAL]
case neg.refine_1
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ IsPrimitive (X ^ n - X - 1)
[PROOFSTEP]
exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive
