best way to cast (i: fin n - 1)into (fin n)

Stream: general

[Shi Zhengyu]

Hi all,

I am wondering what is the best way to cast a (i: fin n - 1) into fin n for some natural number n.
with (ng1: n >= 1), (i: fin n - 1)I am currently using (fin.cast_lt i (lt_trans (fin.is_lt i) (buffer.lt_aux_2 ng1))). it works, but I am not sure it should be this complicated to do such simple task.

Thanks!

[Shi Zhengyu]

(deleted)

[Mario Carneiro]

docs#fin.cast_succ will cast fin n to fin (n+1), which is generally preferable (avoid subtraction)