p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ p ^ i < p ^ n
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ i < n
rw [← pow_lt_iff_lt_right hp]
no goals
p i n : ℕ
hn : n ≠ 0
hp : 2 ≤ p
h : p ^ i ∣ n
⊢ p ^ i < p ^ n
exact lt_of_le_of_lt (le_of_dvd hn.bot_lt h) (lt_pow_self (succ_le_iff.mp hp) n)