[Agda] proofs for (NON)TERMINATING

[Sergei Meshveliani]

Can somebody, please, explain how to express/prove the following lemma? 

-------------------------------------------------------------------
open import Relation.Nullary using (yes; no)
open import Relation.Binary  using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Empty   using (⊥-elim)
open import Data.Product using (_,_; proj₁; ∃)
open import Data.Nat     using (ℕ; suc)

postulate  P  : ℕ → ℕ → Set
           p? : Decidable P

{-# NON_TERMINATING #-}                                               
find : (m : ℕ) → ℕ → ∃ (\k → P m k)
find m n
       with p? m n
...    | yes pmn = (n , pmn)       -- found            
...    | no _    = find m (suc n)  -- try next

lemma :  ∀ m → P m 0 → proj₁ (find m 0) ≡ 0
lemma m pm0
        with p? m 0
...     | yes _   =  refl
...     | no ¬pm0 =  ⊥-elim (¬pm0 pm0)
--------------------------------------------------------------------

For some P above the algorithm `find' is not terminating.
So that this program would not type-check without pragma.
The TERMINATING pragma is wrong to set.
So, NON_TERMINATING is needed (?).

Then, it occurs that `lemma' is not type-checked.
This contradicts to the fact that  (find m 0)  terminates when  (P m 0)
is satisfied.

Is it possible to express and prove in Agda the above lemma? 

Thanks,

------
Sergei