I generate lists with various integer patterns and I'd like to prove that the generated lists hold certain properties. The lemmas refer to the items of the generated lists by their positions. The generator functions receive the desired list length as parameter. Working with induction, the length of the list must be constrained as being greater or equal to 0, so that the positional references are valid, which yields a base induction caselike this:
0 < 0 ... ==> Property(generator(0))
which holds and disappears after apply(simp) but seems to be irrelevant. Would it still be a valid proof provided that the induction step holds too? Is there a better approach?
Yes, the proof is still valid. It's perfectly fine that sometimes in induction proofs some cases are vacuous.