Em Dafny, conte os elementos do conjunto abaixo de um limite

Eu gostaria de contar os elementos em um Dafny que são definidos abaixo de um limite, mas não consigo descobrir o 'garantir'.

method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |{i in numbers | i < threshold}|
{
  count := 0;
  var ss := numbers;
  while ss != {}
    decreases |ss|
  {
    var i: int :| i in ss;
    ss := ss - {i};
    if i < threshold {
      count := count + 1;
    }

  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

O erro é:this operator chain cannot continue with an ascending operator