page 1  1 
We want to prove
( K : NzNat ) K > 0 .We use induction on K to prove this goal. For this, we use the induction scheme based on the signature { 1, s } for NzNat. Induction requires that we do the following:
And thus the main goal is proved. 
