```
Definition mod_fun (first a: nat)(l: list nat) : nat:=
if beq_nat first 0 then a mod (length l) else (a+1) mod (length l).
```

I am using mod_fun in main function f' recusively, whose output is list nat. In main function simply

increase the value of a.(always start first=0 , a=0 , increase a till it becomes equal to length l and only first time

first is zero). Output list nat always contains more zeros than any other natural number.(Because f' always start with zero and get zero when a becomes equal to length l). I want to prove this statement,how to do it?

Last updated: Jun 23 2024 at 04:03 UTC