The Coq mailing list

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

On 11/14/2012 07:15 AM, xavier wrote:
> After a few trivial simple steps, I get the following goal:
>
> P : nat ->  Prop
> dec : forall n : nat, P n \/ ~ P n
> n : nat
> nft : ~ (forall m : nat, m>= n ->  ~ P m)
> ______________________________________(1/1)
> exists m : nat, m>  n /\ P m
>
> This looks rather trivial to me. If it is not the case that all m greater than
> n do not have the property, then I can find one that has for which it holds.
> And yet I'm stuck.
>    

I won't be surprised if your goal still isn't provable without extra 
axioms.  For instance, you'd probably want to use one of the 
classical-logic corollaries here:
    
http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Logic.Classical_Pred_Type.html