Dafny proof to the Container With Most Water Problem

The problem is introduced and proven (manually) here: https://leimao.github.io/blog/Proof-Container-With-Most-Water-Problem/

We’ll do the proof in Dafny.

method maxArea(height: array?<int>) returns (vol: int, maxVol: int)
  requires height != null && 0 < height.Length
  ensures maxVol >= vol
{
  var i  := 0;
  var j  := height.Length - 1;
  maxVol := 0;
  vol    := 0;
  while i < j
    invariant i <= j && j < height.Length && maxVol >= vol
  {
    if height[i] < height[j]
    {
      vol := (j - i) * height[i];
      i := i + 1;
    }
    else
    {
      vol := (j - i) * height[j];
      j := j - 1;
    }
    if vol > maxVol {
      maxVol := vol;
    }
  }
}

Namely, the invariant $i \leq i \land j < |\text{height}| \land \text{maxVol} \geq \text{vol}$ holds for every iteration, whenever $\text{vol} = (j - i) \cdot \text{height}_i$ or $\text{vol} = (j - i) \cdot \text{height}_j$ . Thus, at the end of the iterations, $maxVol$ will contain the largest volume.