apply le_trans (Nat.log_mono_right hnp)
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (2 * n) ≤ 1
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) ≤ 1