no goals
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
⊢ succ p * succ p ^ k ∣ succ p * 1
simpa [pow_succ'] using h
no goals
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝¹ : succ p * succ p ^ k ∣ succ p * 1
this✝ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this : k < succ p ^ k
⊢ k < 1
rwa [he] at this
no goals
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝³ : succ p * succ p ^ k ∣ succ p * 1
this✝² : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝¹ : k < succ p ^ k
this✝ : k < 1
this : k = 0
⊢ 1 < 1
rwa [this] at hk
no goals
p k : ℕ
hp : 1 < succ p
hk : 1 < succ k
h : succ p ^ succ k ∣ succ p
this✝⁴ : succ p * succ p ^ k ∣ succ p * 1
this✝³ : succ p ^ k ∣ 1
he : succ p ^ k = 1
this✝² : k < succ p ^ k
this✝¹ : k < 1
this✝ : k = 0
this : 1 < 1
⊢ ¬1 < 1
decide