Proving a counting slope search algorithm with Dafny

Question

I've been working to implement a slope search algorithm in Dafny where I have a double ascending matrix, and I want to calculate the amount of elements strictly less than a given value. Besides the O(NM) algorithm, I'm looking to implement the linear algorithm. I've gone ahead and implemented a predicate which ensures the matrix is double sorted

I've also fully solved the problem on paper, and have landed on the following pseudo code for it, which I've fully proven formally to be correct.

const m, n, w, matrix;
var x, y, z;

z := 0;
x := 0;
y := n;

while x < m && y > 0 do
  if matrix[y-1][x] < w then 
    z := z + y;
    x := x + 1;
  else
    y := y - 1;
  end;
end;

In Dafny, I've setup the following predicate for a double sorted matrix:

predicate AscAsc(a: array2<int>)
  reads a
{
  (forall i, j, k:: 0 <= i < j < a.Length0 && 0 <= k < a.Length1 ==> a[i,k] <= a[j,k]) &&
  (forall i, j, k:: 0 <= i < a.Length0 && 0 <= j < k < a.Length1 ==> a[i,j] <= a[i,k])
}

And I've also implemented some convenience functions which allow me to use them in specifications

function CountInColumn(a: array2<int>, col:int, ylo: int, yhi: int, value: int): int
  requires 0 <= col < a.Length1
  requires 0 <= ylo <= yhi <= a.Length0
  requires AscAsc(a)
  decreases yhi-ylo
  reads a
{
  if(ylo == yhi) then 0
  else
  if(a[ylo,col] < value) then 1+CountInColumn(a,col,ylo+1,yhi,value)
  else CountInColumn(a,col,ylo+1,yhi,value)
}

function CountInMatrix(a: array2<int>, xlo: int, xhi: int, ylo: int, yhi: int, value: int): int
  requires 0 <= xlo <= xhi <= a.Length1
  requires 0 <= ylo <= yhi <= a.Length0
  requires AscAsc(a)
  decreases xhi-xlo
  reads a
{
  if(xlo == xhi) then 0
  else
    CountInColumn(a,xlo,ylo,yhi,value) + CountInMatrix(a,xlo+1,xhi,ylo,yhi,value)
}

function FastCountInMatrix(a: array2<int>, xlo: int, xhi: int, ylo: int, yhi: int, value: int): int
  requires 0 <= xlo <= xhi <= a.Length1
  requires 0 <= ylo <= yhi <= a.Length0
  requires AscAsc(a)
  reads a
  decreases xhi-xlo + yhi-ylo
{
  if(xlo == xhi) then 0
  else if(ylo == yhi) then 0
  else if(a[ylo,xlo] < value) then
    yhi - ylo + FastCountInMatrix(a,xlo+1,xhi,ylo,yhi,value)
  else
    FastCountInMatrix(a,xlo,xhi,ylo,yhi-1,value)
}

lemma FastCountInMatrixLemma(a: array2<int>, xlo: int, xhi: int, ylo: int, yhi: int, value: int)
  requires 0 <= xlo <= xhi <= a.Length1
  requires 0 <= ylo <= yhi <= a.Length0
  requires AscAsc(a)
  ensures FastCountInMatrix(a,xlo,xhi,ylo,yhi,value) == CountInMatrix(a,xlo,xhi,ylo,yhi,value)
  decreases xhi-xlo + yhi-ylo

I've also assumed FastCountInMatrix to be equal to CountInMatrix, as I'm unsure how I'd go about proving that.

I've then translated the pseudo code directly into Dafny as such

method StudentImplementation(a: array2<int>, value: int) returns (z: int)
  requires AscAsc(a)
  requires a.Length0 > 0 && a.Length1 > 0
  ensures z == CountInMatrix(a,0,a.Length1,0,a.Length0,value)
{
  z := 0;

  var x := 0;
  var y := a.Length0;

  while(x < a.Length1 && y > 0)
    invariant 0 <= x <= a.Length1
    invariant 0 <= y <= a.Length0
    invariant z == FastCountInMatrix(a, 0, x, y, a.Length0, value)
    decreases a.Length1 + y - x
  {

    if(a[y - 1,x] < value) {
      z := z + y;
      x := x + 1;
    } else {
      y := y - 1;
    }
  }
}

Although Dafny appears unable to prove this. How could I go about implementing something which Dafny can prove?

I've tried going through the relevant literature (specifically Program Proofs by K. Rustan and M. Leino), which is how I came up with the AscAsc predicate, and have based my code mostly on the slope search which looks for the existence of a value, rather than counting everything under it.

Looking through Dafny counterexamples, and peppering it with asserts has also not lead me anywhere.