method Upto_stronger(n: int) returns (r: seq<int>)
  requires n >= 0
  ensures |r| == n
  ensures forall i :: 0 <= i < n-1 ==> r[i] <= r[i+1]
  ensures forall v :: v in r ==> 0 <= v < n
{
  if n == 0 {
    return [];
  } else {
    var t := Upto_stronger(n-1);

    // (3) Try to keep going!

    // (2) Then work backward. Try splitting the implication into 2 cases:
    //  - what do we need when `i` is in bounds for `t`? (i.e. 0 <= i < n-2)
    // assert forall i :: 0 <= i < n-2 ==> ???;
    //  - what do we need when `i == n-2`? (which is only possible when n > 1)
    // assert n > 1 ==> ???;

    // (1) Re-state postcondition that we couldn't prove:
    // assert forall i :: 0 <= i < n-1 ==> (t + [n-1])[i] <= (t + [n-1])[i+1];

    return t + [n-1];
  }
}