function Pow(n: nat): int
  decreases n
{
  if n == 0 then 1 else 2 * Pow(n - 1)
}

// Keep `decreases n` and repair the proof (copied from what we just saw together) so that it checks out.

lemma PowPlusDist(m: nat, n: nat)
  ensures Pow(m + n) == Pow(m) * Pow(n)
  decreases n
{
  if m == 0 {
  } else {
    calc {
      Pow(m) * Pow(n);
      2 * Pow(m - 1) * Pow(n);
      2 * (Pow(m - 1) * Pow(n));
      { PowPlusDist(m - 1, n); } // here is the recursive call; notice that our termination metric goes down
      2 * Pow(m + n - 1);
      Pow(m + n);
    }
  }
}