function Mult(x: nat, y: nat): nat {
  if y == 0 then 0 else x + Mult(x, y - 1)
}

// Fill in the two missing cases of this fairly manual proof by induction.
lemma {:induction false} MultCommutative(x: nat, y: nat)
  ensures Mult(x, y) == Mult(y, x)
  decreases x, y
{
  if x == y {
  } else if x == 0 {
    assert Mult(x, y) == Mult(x, y - 1);
    assert Mult(y, x) == 0 == Mult(y - 1, x);
    MultCommutative(x, y - 1);
  } else if y < x {
    // Our proof invokes the induction hypothesis *once* here.
  } else {
    // Our proof invokes the induction hypothesis *three times* here.
    // (Weird, right?)
  }
}