PartialSups in a SuccAddOrder

@[simp]

theorem partialSups_add_one {α : Type u_1} {ι : Type u_2} [SemilatticeSup α] [Add ι] [One ι] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccAddOrder ι] (f : ι → α) (i : ι) : (partialSups f) (i + 1) = (partialSups f) i ⊔ f (i + 1)