The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

It's easy to prove a lemma showing that, for any property of the natural 
numbers, if there exists a number that satisfies it, then there also 
exists a minimum number that satisfies it.  You would then apply the 
lemma to transform your hypothesis before eliminating it.

On 11/26/2015 11:06 AM, David Asher wrote:
> Hey Coq-Club,
>
> I'm trying to prove a theorem in Coq for which I have got a proof in 
> pencil and paper form. Unfortunately I'm stuck because in the proof 
> there is a step for which
> I haven't been able to find an equivalent in Coq. Somewhere during the 
> proof session I have an existential proposition H in the context, i.e.
>
> H: exists n : nat, P n
>
> for some Prop P. In my pencil and paper proof I'm "instantiating" the 
> existential variable as the smallest n, such that the Proposition 
> holds. I am aware that
> it is possible to "instatiate" an existential proposition in the 
> context with
>
> destruct H as [n]
>
> This, however, just creates a fresh variable n in the context and 
> "instantiates" the existential proposition with the freshly created 
> variable. But I need some
> additional information [ somethig like "~ (exists m, m < n /\ P m)" ] 
> in the context. Any ideas how to solve this?
>
> Thanks
> David