Hi,

I am working on the following proof that ∀ n, ⟦0, n⟧ is finite (for “finite” defined as "no injection from ℕ to this type”). Please note that there could be more elegant definitions, stdlib use, etc. but my goal is more to increase my understanding of Coq than to do this fast

I have omitted parts of the proof that are not relevant here, using `admit`

.

While I can see other ways, I went for an inductive proof.

```
Require Import PeanoNat.
Require Import ProofIrrelevance.
Definition iv (n : nat) : Type := {a : nat | a <= n}.
Definition injective {X Y : Type} (f : X -> Y) : Prop := forall x x' : X, f x = f x' -> x = x'.
Definition finite (X : Type) : Prop := ~(exists f : nat -> X, injective f).
Lemma iv_finite (n : nat) : finite (iv n).
Proof.
induction n as [|n Hn].
* admit.
* intro. destruct H as [f Hf]. apply Hn. clear Hn.
assert (exists N, forall m, N <= m -> proj1_sig (f m) <> S n) by admit.
destruct H as [N HN].
unshelve eexists (fun (p : nat) => _ : iv n). {
set (i := p+N).
assert (H : N <= i) by apply Nat.le_add_l.
apply HN in H.
destruct (f i) as [fi Hfi].
exists fi. now apply le_S_n, Nat.le_neq.
}
intros x x' H. inversion H. clear H.
```

At this point, the proof state looks like this:

```
n : nat
f : nat -> iv (S n)
Hf : injective f
N : nat
HN : forall m : nat, N <= m -> proj1_sig (f m) <> S n
x, x' : nat
H1 : (let (x, p) as s return (proj1_sig s <> S n -> iv n) := f (x + N) in
fun H : x <> S n =>
exist (fun a : nat => a <= n) x
(le_S_n x n (match Nat.le_neq x (S n) with
| conj _ x1 => x1
end (conj p H)))) (HN (x + N) (Nat.le_add_l N x)) =
(let (x, p) as s return (proj1_sig s <> S n -> iv n) := f (x' + N) in
fun H : x <> S n =>
exist (fun a : nat => a <= n) x
(le_S_n x n (match Nat.le_neq x (S n) with
| conj _ x1 => x1
end (conj p H)))) (HN (x' + N) (Nat.le_add_l N x'))
============================
x = x'
```

I want to prove `f (x + N) = f (x' + N)`

, which implies `x = x'`

by `Hf`

(`f`

injective). If you squint at this big equality `H1`

, you can see that it says essentially this, plus equality of some proofs. In each of the members, `f (x + N)`

(resp. `f (x' + N)`

is destructed with `let`

as `(x, p)`

, and the term built up is `exist ... x ...`

. I just want to set the third element of the `exist`

(the proof of existence) and keep the equality of the second element (the witness). However, I was not able to do that. I tried variants of `destruct (f (x + N))`

, which fails while abstracting because the term `f (x + N)`

occurs in the types in the proof I want to discard. Also, I don’t fully understand why this term `(let (x, p) as s return ... in fun H => ...) (...)`

is not reduced by `compute`

into `(let (x, p) as s return ... in let H := ... in ...)`

or something similar.