Chapter 2 and A3q4

soooo I'm reading through  Chapter 2 about loop invariants, working through proving a binary search algorithm for A3q4 and I come across something in the inductive step for such a proof that reads:

"If there is no (j + 1)-st iteration then P(j + 1) holds trivially. So, assume that there is such an iteration."

p 52 internal, p 60 of the pdf.

And I'm sitting there like if there is no (j + 1)-st iteration, why on earth are we concerned with it. Unable to figure out why this needed to be included in the proof, and knowing that Vassos probably had a good reason to put it there, I turned to piazza to ask the question.

I start writing, and then I get to the part where I'm saying -

           Do we really need to include this?

           I'm having trouble figuring out why it's necessary, especially because in the
           definition of P(i) it states -

   

           P(i) : if the loop is executed at least i times, then...

And then it hits me.  The predicate reads  "*if* the loop is executed at least i times."
So if there is no (j+1)-st iteration, then the conditional proposition that is P(j+1) is indeed vacuously true.

*lightbulb moment*