theorem Fin.pos {n : Nat} (i : Fin n) : 0 < n

@[inline]

def Fin.last (n : Nat) : Fin (n + 1)

The greatest value of Fin (n+1).

@[inline]

def Fin.castLT {m : Nat} {n : Nat} (i : Fin m) (h : i.val < n) : Fin n

castLT i h embeds i into a Fin where h proves it belongs into.

@[inline]

def Fin.castLE {n : Nat} {m : Nat} (h : n ≤ m) (i : Fin n) : Fin m

castLE h i embeds i into a larger Fin type.

@[inline]

def Fin.cast {n : Nat} {m : Nat} (eq : n = m) (i : Fin n) : Fin m

cast eq i embeds i into an equal Fin type.

@[inline]

def Fin.castAdd {n : Nat} (m : Nat) : Fin n → Fin (n + m)

castAdd m i embeds i : Fin n in Fin (n+m). See also Fin.natAdd and Fin.addNat.

@[inline]

def Fin.castSucc {n : Nat} : Fin n → Fin (n + 1)

castSucc i embeds i : Fin n in Fin (n+1).

def Fin.addNat {n : Nat} (i : Fin n) (m : Nat) : Fin (n + m)

addNat m i adds m to i, generalizes Fin.succ.

def Fin.natAdd {m : Nat} (n : Nat) (i : Fin m) : Fin (n + m)

natAdd n i adds n to i "on the left".

@[inline]

def Fin.rev {n : Nat} (i : Fin n) : Fin n

Maps 0 to n-1, 1 to n-2, ..., n-1 to 0.

@[inline]

def Fin.subNat {n : Nat} (m : Nat) (i : Fin (n + m)) (h : m ≤ i.val) : Fin n

subNat i h subtracts m from i, generalizes Fin.pred.

@[inline]

def Fin.pred {n : Nat} (i : Fin (n + 1)) (h : i ≠ 0) : Fin n

Predecessor of a nonzero element of Fin (n+1).

def Fin.clamp (n : Nat) (m : Nat) : Fin (m + 1)

min n m as an element of Fin (m + 1)