∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α} [NoMinOrder α], a ≤ b → insert (a - 1) (Finset.Ico a b) = Finset.Ico (a - 1) b