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_reducible]

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_reducible]

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

theorem Fin.orderSucc_lt_iff {n : ℕ} {i j : Fin n} : Order.succ j < i ↔ ↑j + 1 < ↑i

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

theorem Fin.lt_orderPred_iff {n : ℕ} {i j : Fin n} : i < Order.pred j ↔ ↑i + 1 < ↑j