instance Fin.coeToNat {n : Nat} : CoeOut (Fin n) Nat

def Fin.elim0 {α : Sort u} : Fin 0 → α

def Fin.succ {n : Nat} : Fin n → Fin (Nat.succ n)

def Fin.ofNat {n : Nat} (a : Nat) : Fin (Nat.succ n)

def Fin.ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n

def Fin.add {n : Nat} : Fin n → Fin n → Fin n

def Fin.mul {n : Nat} : Fin n → Fin n → Fin n

def Fin.sub {n : Nat} : Fin n → Fin n → Fin n

Remark: mod/div/modn/land/lor can be defined without using (% n), but we are trying to minimize the number of Nat theorems needed to boostrap Lean.

def Fin.mod {n : Nat} : Fin n → Fin n → Fin n

def Fin.div {n : Nat} : Fin n → Fin n → Fin n

def Fin.modn {n : Nat} : Fin n → Nat → Fin n

def Fin.land {n : Nat} : Fin n → Fin n → Fin n

def Fin.lor {n : Nat} : Fin n → Fin n → Fin n

def Fin.xor {n : Nat} : Fin n → Fin n → Fin n

def Fin.shiftLeft {n : Nat} : Fin n → Fin n → Fin n

def Fin.shiftRight {n : Nat} : Fin n → Fin n → Fin n

instance Fin.instAddFin {n : Nat} : Add (Fin n)

instance Fin.instSubFin {n : Nat} : Sub (Fin n)

instance Fin.instMulFin {n : Nat} : Mul (Fin n)

instance Fin.instModFin {n : Nat} : Mod (Fin n)

instance Fin.instDivFin {n : Nat} : Div (Fin n)

instance Fin.instAndOpFin {n : Nat} : AndOp (Fin n)

instance Fin.instOrOpFin {n : Nat} : OrOp (Fin n)

instance Fin.instXorFin {n : Nat} : Xor (Fin n)

instance Fin.instShiftLeftFin {n : Nat} : ShiftLeft (Fin n)

instance Fin.instShiftRightFin {n : Nat} : ShiftRight (Fin n)

instance Fin.instOfNatFinHAddNatInstHAddInstAddNatOfNat {n : Nat} {i : Nat} : OfNat (Fin (n + 1)) i

instance Fin.instInhabitedFinHAddNatInstHAddInstAddNatOfNat {n : Nat} : Inhabited (Fin (n + 1))

theorem Fin.val_ne_of_ne {n : Nat} {i : Fin n} {j : Fin n} (h : i ≠ j) : i.val ≠ j.val

theorem Fin.modn_lt {n : Nat} {m : Nat} (i : Fin n) : m > 0 → (Fin.modn i m).val < m

theorem Fin.val_lt_of_le {n : Nat} {b : Nat} (i : Fin b) (h : b ≤ n) : i.val < n

instance instGetElemFinVal {cont : Type u_1} {elem : Type u_2} {dom : cont → Nat → Prop} {n : Nat} [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i.val