Is Loop Invariant Proof a form of Induction?
Good question. I think yes, a loop invariant proof implies induction. However, it also deals with the termination step which is outside of the scope of induction. So a loop invariant contains an induction proof, but goes beyond that, and so an induction proof does not do all that a loop invariant proof does.


  (1) Here, showing that the invariant holds before the first iteration is like the
  base case, and showing that the invariant holds from iteration to iteration
  is like the inductive step.