Obviously, the set of nonnegative integers below n has cardinality n. But dafny seemingly can't prove it:

method FirstNonnegatives(n: int) returns (s: set)
    requires n >= 0
    ensures |s| == n
{
    s := set k | 0 <= k < n;
}

What change would help the verifier with the method above?