Fin k -> Fin (k + n)

Stream: Is there code for X?

[Sofia]

Is there a function to transform Fin k -> Fin (k + n)? I have found Nat.le_add_right (n m : Nat) : n <= n + m. More generally I am after a function from n < k -> n < k + m. Cannot find either such function. :/

[Anne Baanen]

In mathlib 3 the map on fin is docs#fin.cast_add and your proof is either docs#lt_add_of_nonneg_of_lt combined with docs#nat.zero_le or docs#lt_of_lt_of_le combined with docs#nat.le_add_right. I'd expect you can find these results for Lean 4 as well (with appropriate renaming).