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