The Coq mailing list

[David Asher <asher AT informatik.hu-berlin.de>]

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