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

Require Import Psatz Arith.  (* use lia to solve the linear integer arithmetic. *)

Variable f : nat -> nat.

This below is essentially your goal, modulo packing of the statement into some dependent type. (It doesn't say that mi < n, but you can extend the proof statement to also contain that.)

Goal forall n, exists mi, forall i, i < n -> f mi <= f i.

  induction n; intros.
  - now exists 0; inversion 1. (* n cant be zero *)
  - destruct IHn as [mi IHn].  (* get the smallest pos mi, which is < n *)
    (* Is f mi still smallest, or is f n the smallest? *)    
    (* If f mi < f n then mi is the position of the 
       smallest value, otherwise n is that position,
       so consider those two cases. *)
    destruct (lt_dec (f mi) (f n));
      [ exists mi |  exists n];
      intros.

    + destruct (eq_nat_dec i n).
      subst; lia.
      apply IHn; lia.

    + destruct (eq_nat_dec i n).
      subst; lia.
      apply le_trans with(f mi).
      lia.
      apply IHn.
      lia.
Qed.