function TriangleNumber(n: int): int
  requires 0 <= n
{
  if n == 0 then 0 else TriangleNumber(n - 1) + n
}

function SumCubesThrough(n: nat): nat {
  if n == 0 then 0 else SumCubesThrough(n - 1) + n * n * n
}

lemma Sums(n: nat)
  ensures TriangleNumber(n) * TriangleNumber(n) == SumCubesThrough(n)
{
  if n == 0 {
  } else {
    // For brevity, here are names for things with long names
    var tn := TriangleNumber(n);
    var tn' := TriangleNumber(n - 1);
    var s' := SumCubesThrough(n - 1);
    // Pro tip: Working with non-linear arithmetic can require a lot of patience with the verifier.
    // Sometimes, it can help to name subexpressions, so we introduce the name "nn" here.
    var nn := n * n;

    // Fill in the remainder of a proof here.
  }
}