The Coq mailing list

[staecker<cstaecker AT fairfield.edu>]

I'm new to Coq- trying to learn some basics. 

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). 

I tried to find something like this in the standard library, but the closest I
found was:
Lemma dec_inh_nat_subset_has_unique_least_element :
  forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
    (exists n, P n) -> has_unique_least_element le P.

which requires an extra decidability condition as well. Is there a stronger
version somewhere which doesn't require decidability? Is my version of the
theorem even true?

Thanks- chris