The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

> I need to use a theorem like this:
> Lemma nat_well_ordered: forall (P:nat -> Prop),
>  (exists n:nat, P n) -> (exists m:nat, P m /\
>    forall k:nat, P k -> k >= m).

Consider the fact that Coq's logic is intuitionistic, and try to think
of this theorem of yours in a constructive manner. If you're given an
n for which P is true, then how are you gonna compute the smallest k
for which P is true?
Indeed, you need to be able to decide if P is true on a given m to
write such a function.  This is why you need the decidability of P to
prove this theorem.

If you're not interested in constructive logic, just assume the
excluded middle and using it you can use prove your theorem by a
simple induction on n.

HTH,
Stéphane
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06