K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
h1 : degree X < degree (X ^ p)
⊢ natDegree (X ^ p - X) = p
K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ natDegree (X ^ p - X) = p
have h1 : (X : K'[X]).degree < (X ^ p : K'[X]).degree := by
  rw [degree_X_pow, degree_X]
  exact WithBot.coe_lt_coe.2 hp
no goals
K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
h1 : degree X < degree (X ^ p)
⊢ natDegree (X ^ p - X) = p
rw [natDegree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), natDegree_X_pow]
K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ 1 < ↑p
K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ degree X < degree (X ^ p)
rw [degree_X_pow, degree_X]
no goals
K : Type ?u.726863
R : Type ?u.726866
inst✝² : Field K
inst✝¹ : Fintype K
K' : Type u_1
inst✝ : Field K'
p n : ℕ
hp : 1 < p
⊢ 1 < ↑p
exact WithBot.coe_lt_coe.2 hp