Successors in intervals

If j is an element of a partially ordered set equipped with a successor function, then for any element i : Set.Iic j which is not the maximum, we have ↑(Order.succ i) = Order.succ ↑i.

theorem Set.Iic.coe_succ_of_not_isMax {J : Type u_1} [PartialOrder J] [SuccOrder J] {j : J} {i : ↑(Iic j)} (hi : ¬IsMax i) : ↑(Order.succ i) = Order.succ ↑i

theorem Set.Iic.succ_eq_of_not_isMax {J : Type u_1} [PartialOrder J] [SuccOrder J] {j : J} {i : ↑(Iic j)} (hi : ¬IsMax i) : Order.succ i = ⟨Order.succ ↑i, ⋯⟩

theorem Set.Ici.coe_pred_of_not_isMin {J : Type u_1} [PartialOrder J] [PredOrder J] {j : J} {i : ↑(Ici j)} (hi : ¬IsMin i) : ↑(Order.pred i) = Order.pred ↑i

theorem Set.Ici.pred_eq_of_not_isMin {J : Type u_1} [PartialOrder J] [PredOrder J] {j : J} {i : ↑(Ici j)} (hi : ¬IsMin i) : Order.pred i = ⟨Order.pred ↑i, ⋯⟩