[Agda] termination proof problem

[Sergei Meshveliani]

On Mon, 2016-03-28 at 16:46 +0300, Sergei Meshveliani wrote:
> Here is a concrete example.
> Goal: find the first prime after a given prime  p : ℕ.
> 
>  firstPrimeAfter :  
>       (p : ℕ) → IsPrime p → 
>                 (∃ \q →  p < q  ×  IsPrime q  ×  NoPrimeBetween p q)
> [..]

>  bound p = let ps = p1, p2, ..., p   -- all primes up to p
>                a  = product ps       -- = p1 * p2 * ... * p
>                b  = 1 + a
>            in
>            firstNonUnityFactor b
> 


> It is proved in Agda that  p < bound p  and  IsPrime p.
> [..]


Sorry, fixing a typo:   

 It is proved in Agda that  p < bound p  and  IsPrime (bound p).


------
Sergei