Here's an Agda example of what I think you're suggesting. Note that in `example` I can just use the first element of the pair like a typical number, but I can *also* still use the proof that it's even!
getNthEven : ℕ → ∃[ n ] IsEven n
getNthEven 0 = 0 , IsEven-Z
getNthEven (suc n) =
let m , prf = getNthEven n
in
suc (suc m) , IsEven-SS prf
take : ℕ → List A → List A
take n [] = []
take zero _ = []
take (suc n) (x ∷ xs) = x ∷ take n xs
safeDiv2 : (n : ℕ) → IsEven n → ℕ
safeDiv2 n IsEven-Z = 0
safeDiv2 (suc (suc n)) (IsEven-SS nIsEven) =
suc (safeDiv2 n nIsEven)
add5 : ℕ → ℕ
add5 n = n 5
example : ℕ
example =
let n , nIsEven = getNthEven 2
in
add5 n * safeDiv2 n nIsEven