Re: [isabelle] Induction over n for a proposition ALL k <= n



> At the moment, I am using
> 
> theorem
>   "(⋀k. ⟦ k < n; P i (i+k) ⟧ ⟹ Q i (i+k)) ⟹ P i (i+n) ⟹ Q i (i+n)"
> 
> This seems to be rather convoluted, though. What is the usual approach here?

I should add that I have no idea whether this works, as I'm still in the
process of figuring out how my proof should look like.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.