# Zulip Chat Archive

## Stream: new members

### Topic: fin succ proof coercing to `n + 1`

#### Yakov Pechersky (Jul 28 2020 at 19:46):

Is there some `fin n`

coercion lemma that is missing? Or should I be using `fin.cast_succ`

? In the following proof. I don't know how to remove `% (n + 1)`

even if I have a hypothesis of `i < n`

.

```
import tactic.linarith
example {n : ℕ} (i : fin n) : ((i : fin (n + 1)) + 1) = i.succ :=
begin
cases i with i h,
induction i with k hk,
simp [fin.succ],
cases n, linarith, refl,
cases n, linarith,
simp [fin.succ],
/-
case nat.succ, nat.succ
k n : ℕ,
hk : ∀ (h : k < n.succ), ↑⟨k, h⟩ + 1 = ⟨k, h⟩.succ,
h : k.succ < n.succ
⊢ ↑k + 1 + 1 = ⟨k.succ.succ, _⟩
-/
sorry,
end
```

#### Yakov Pechersky (Jul 28 2020 at 20:15):

Even this is confusing me. I'm unable to use `h`

with `hi`

.

```
example (i n : ℕ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
induction i with i hi,
simp,
sorry,
end
```

#### Kevin Buzzard (Jul 28 2020 at 20:48):

I don't think you need induction to prove this. There's bound to be a lemma in the library saying that if i<j then i%j=i, it will be called mod_lt or something

#### Jalex Stark (Jul 28 2020 at 20:50):

the code you posted doesn't say anything about `%`

#### Kevin Buzzard (Jul 28 2020 at 20:53):

Addition on fin uses % IIRC

#### Johan Commelin (Jul 28 2020 at 20:59):

I would avoid the cast from `nat`

to `fin (n+1)`

. It isn't "nice" (imho)

#### Johan Commelin (Jul 28 2020 at 21:00):

But if you really need to, you can do it. The file `zmod.lean`

will show you how to deal with it.

#### Jalex Stark (Jul 28 2020 at 21:03):

I had to guess that the lemma I wanted started with `fin.coe_`

. I spent about a minute trying other things before making this guess.

```
example (i n : ℕ) (h : i < n) : (i : fin (n + 1)).val = i :=
begin
apply fin.coe_coe_of_lt, linarith,
end
```

Last updated: May 13 2021 at 18:26 UTC