Eliminating into Prop woes

Stream: maths

[Koundinya Vajjha]

I have defined the following

import algebra.archimedean

def pow_two_near (n : ℤ) : (n > 1) → ∃ k : ℕ, (2 ^ k ≤ n ∧ n < 2^(k+1)) :=
by intro h ; exact (exists_nat_pow_near h one_lt_two)

Is there any way to get ahold of the k without doing this?

noncomputable def index_pow_two_near (n : ℤ) (h : n > 1) : ℕ := classical.some $ pow_two_near n h

If I try to destruct the exists I get an error:

def index_pow_two_near' (n : ℤ) (h : n > 1) : ℕ :=
begin
have h := pow_two_near n h,
cases h, --induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
end

[Johan Commelin]

@Koundinya Vajjha Try choose k hk using h.

[Koundinya Vajjha]

Thanks Johan