fin 0 is empty

The greatest value of fin (n+1)

cast_lt i h embeds i into a fin where h proves it belongs into.

cast_le h i embeds i into a larger fin type.

cast eq i embeds i into a equal fin type.

cast_add m i embedds i in fin (n+m).

cast_succ i embedds i in fin (n+1).

succ_above p i embeds into fin (n + 1) with a hole around p.

pred_above p i h embeds i into fin n by ignoring p.

sub_nat i h subtracts m from i, generalizes fin.pred.

add_nat i h adds m on i, generalizes fin.succ.

nat_add i h adds n on i