[Agda] termination proof problem

[Sergei Meshveliani]

On Sun, 2016-03-27 at 23:56 +0400, Sergei Meshveliani wrote:
> Can people explain, please, the following subject concerning termination
> proof tools?
> 
> Having certain 
>                    P : ℕ → Set  and   P? : Decidable P,	
> 
> one needs to implement
> 
>     search :  (n : ℕ) → ∃ \y →  m < y × P y × IsMinimalSuch y
> 
> -- find the first  y  after  m  such that  P y.                       
> [..]


Fixing a typo:  replace  "m"  with  "n"  in these two lines.


------
Sergei