Conditions for Fin.insertNth to be monotone or strictly monotone

theorem Fin.insertNth_zero_monotone {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : Monotone f) (x : α) (hx : x ≤ f 0) : Monotone (insertNth 0 x f)

theorem Fin.strictMono_insertNth_zero {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : StrictMono f) (x : α) (hx : x < f 0) : StrictMono (insertNth 0 x f)

theorem Fin.insertNth_monotone {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : Monotone f) (i : Fin n) (x : α) (hx₁ : f i.castSucc ≤ x) (hx₂ : x ≤ f i.succ) : Monotone (i.castSucc.succ.insertNth x f)

theorem Fin.strictMono_insertNth {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : StrictMono f) (i : Fin n) (x : α) (hx₁ : f i.castSucc < x) (hx₂ : x < f i.succ) : StrictMono (i.castSucc.succ.insertNth x f)

theorem Fin.insertNth_last_monotone {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : Monotone f) (x : α) (hx : f (last n) ≤ x) : Monotone ((last (n + 1)).insertNth x f)

theorem Fin.strictMono_insertNth_last {n : ℕ} {α : Type u_1} [Preorder α] {f : Fin (n + 1) → α} (hf : StrictMono f) (x : α) (hx : f (last n) < x) : StrictMono ((last (n + 1)).insertNth x f)