[Agda] using Induction.Nat

[Sergei Meshveliani]

People,
I have this program for powering  x^(n+1)  
for  x : Carrier of a Semigroup: 

 half : ℕ → ℕ
 half = ⌊_/2⌋

 powerTo-suc : C → (e : ℕ) → C     -- x^(e+1)  
 powerTo-suc x 0       = x            
 powerTo-suc x (suc e) = case  even? e  of \ 
                                        { (yes _) → p ∙ p 
                                        ; _       → x ∙ (p ∙ p) }
                                        where  
                                        h = half e 
                                        p = powerTo-suc x h

The checker cannot prove its termination.
I can help this proof by adding the counter argument  cnt  for the
number of the  `half'  calls.   
But this complicates various further proofs for  powerTo-suc.

So, I think of trying _inductive families_ for  ℕ  provided by
Induction, Induction.Nat ... in the standard library
(the question of whether this will make further proofs easier is open
for me).

But it is difficult to understand the idea, some introductory text is
needed, with a couple of simple examples.

Induction.Nat  gives an example for  `half'. It is too simple, because
it is for the step from  n  to  suc n.
And in my example, it is the step from  half (suc e)  to  suc e,
assuming that we have a proof for  
                                  half (suc e) < suc e.

Probably  cRec  needs here to be given something additional, maybe some
builder needs to be defined.

May be you can demonstrate this Agda induction right on this example of
powerTo-suc ?

Thank you in advance for explanation.

------
Sergei