calc
  _ ≤ Nat.log p n := by
    apply Nat.le_log_of_pow_le hp.one_lt hpkn.le
  _ ≤ Nat.log 2 n := by
    apply Nat.log_anti_left (by norm_num) hp.two_le
  _ ≤ Nat.log 2 N := by
    apply Nat.log_mono_right hnN.le
case neg.h.refine_2
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
hnN : n < N
p k : ℕ
hp : p.Prime
hk_pos : 0 < k
hpkn : p ^ k = n
hk : ¬k = 1
⊢ k ≤ Nat.log 2 N
no goals