SuccOrder and PredOrder of Fin n

In this file, we show that Fin n is both a SuccOrder and a PredOrder. Note that they are also archimedean, but this is derived from the general instance for well-orderings as opposed to a specific Fin instance.

instance Fin.instSuccOrder {n : ℕ} : SuccOrder (Fin n)

theorem Fin.orderSucc_eq {n : ℕ} : Order.succ = fun (i : Fin (n + 1)) => lastCases (last n) succ i

theorem Fin.orderSucc_apply {n : ℕ} (i : Fin (n + 1)) : Order.succ i = lastCases (last n) succ i

@[simp]

theorem Fin.orderSucc_last (n : ℕ) : Order.succ (last n) = last n

@[simp]

theorem Fin.orderSucc_castSucc {n : ℕ} (i : Fin n) : Order.succ i.castSucc = i.succ

instance Fin.instPredOrder {n : ℕ} : PredOrder (Fin n)

theorem Fin.orderPred_eq {n : ℕ} : Order.pred = fun (i : Fin (n + 1)) => cases 0 castSucc i

theorem Fin.orderPred_apply {n : ℕ} (i : Fin (n + 1)) : Order.pred i = cases 0 castSucc i

@[simp]

theorem Fin.orderPred_zero (n : ℕ) : Order.pred 0 = 0

@[simp]

theorem Fin.orderPred_succ {n : ℕ} (i : Fin n) : Order.pred i.succ = i.castSucc