The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Lucian M. Patcas wrote:
> My question is what's the strategy to prove this lemma
>
> forall t : nat, t >=2 -> t <= 1000 -> f t
>
> in Coq, assuming f t holds over that interval.

I wouldn't say there is a well-defined strategy for all lemmas of that 
form.  For instance, consider [f] that ignores its argument and always 
returns "P <> NP".