Using result of if condition inside itself

Stream: Is there code for X?

[shortc1rcuit]

I'm trying to generate a function of the type Fin (k + 1) ↦ Fin (k + 1) using a function of the type Fin k ↦ Fin k (which is called b). It should be of the form n ↦ if n = 0 then 0 else b (n - 1) + 1. However n - 1 needs to be cast from Fin (k + 1) to Fin k. This needs a proof that n - 1 < k, which needs a proof that 1 ≤ n which can be derived from the fact that as we are in the else branch, n ≠ 0. How do I get this fact?

[Ruben Van de Velde]

Are you looking for if h : n = 0...?

[shortc1rcuit]

In hindsight I probably should have tried that. Thanks for the help!

[Yury G. Kudryashov]

See docs#ite and docs#dite for the functions behind these notations.