Minimum in non-empty, finite set

Question

With the following definitions I want to prove lemma without_P

Variable n : nat.
Definition mnnat := {m : nat | m < n}.
Variable f : mnnat -> nat.

Lemma without_P : (exists x : mnnat, True) -> (exists x, forall y, f x <= f y).

Lemma without_P means: if you know (the finite) set mnnat is not empty, then there must exist an element in mnnat, that is the smallest of them all, after mapping f onto mnnat.
We know mnnat is finite, as there are n-1 numbers in it and in the context of the proof of without_P we also know mnnat is not empty, because of the premise (exists x : mnnat, True).
Now mnnat being non-empty and finite "naturally/intuitively" has some smallest element (after applying f on all its elements).

At the moment I am stuck at the point below, where I thought to proceed by induction over n, which is not allowed.

1 subgoal  
n : nat  
f : mnnat -> nat  
x : nat  
H' : x < n  
______________________________________(1/1)  

exists (y : nat) (H0 : y < n),
  forall (y0 : nat) (H1 : y0 < n),
  f (exist (fun m : nat => m < n) y H0) <= f (exist (fun m : nat => m < n) y0 H1)

My only idea here is to assert the existance of a function f' : nat -> nat like this: exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f' (exist (fun m : nat => m < n) x H0) = f x, after solving this assertion I have proven the lemma by induction over n. How can I prove this assertion?

Is there a way to prove "non-empty, finite sets (after applying f to each element) have a minimum" more directly? My current path seems too hard for my Coq-skills.

Answer 1

I found a proof to my assertion (exists (f' : nat -> nat), forall (x : nat) (H0: x < n), f (exist (fun m : nat => m < n) x H0) = f' x). by proving the similar assertion (exists (f' : nat -> nat), forall x : mnnat, f x = f' (proj1_sig x)). with Lemma f'exists. The first assertion then follows almost trivially.
After I proved this assertion I can do a similar proof to user larsr, to prove Lemma without_P.

I used the mod-Function to convert any nat to a nat smaller then n, apart from the base case of n = 0.

Lemma mod_mnnat : forall m,
  n > 0 -> m mod n < n.
Proof.
  intros.
  apply PeanoNat.Nat.mod_upper_bound.
  intuition.
Qed.

Lemma mod_mnnat' : forall m,
  m < n -> m mod n = m.
Proof.
  intros.
  apply PeanoNat.Nat.mod_small.
  auto.
Qed.

Lemma f_proj1_sig : forall x y,
  proj1_sig x = proj1_sig y -> f x = f y.
Proof.
  intros.
  rewrite (sig_eta x).
  rewrite (sig_eta y).
  destruct x. destruct y as [y H0].
  simpl in *.
  subst.
  assert (l = H0).
  apply proof_irrelevance. (* This was tricky to find. 
    It means two proofs of the same thing are equal themselves. 
    This makes (exist a b c) (exist a b d) equal, 
    if c and d prove the same thing. *)
  subst.
  intuition.
Qed.


(* Main Lemma *)
Lemma f'exists :
  exists (ff : nat -> nat), forall x : mnnat, f x = ff (proj1_sig x).
Proof.
  assert (n = 0 \/ n > 0).
  induction n.
  auto.
  intuition.
  destruct H.
  exists (fun m : nat => m).
  intuition. destruct x. assert (l' := l). rewrite H in l'. inversion l'.
  unfold mnnat in *.

  (* I am using the mod-function to map (m : nat) -> {m | m < n} *)
  exists (fun m : nat => f (exist (ltn n) (m mod n) (mod_mnnat m H))).
  intros.
  destruct x.
  simpl.
  unfold ltn.
  assert (l' := l).
  apply mod_mnnat' in l'.

  assert (proj1_sig (exist (fun m : nat => m < n) x l) = proj1_sig (exist (fun m : nat => m < n) (x mod n) (mod_mnnat x H))).
  simpl. rewrite l'.
  auto.
  apply f_proj1_sig in H0.
  auto.
Qed.