dafny verifies function with sets but not with multisets

Playing around with the example of Sum and SumMyWay from the dafny power user paper. I noticed that changing from addition to multiplication will work for sets. However, the lemma fails to verify for multisets. Why is this the case and how can it be fixed?

Verifies ok...

function Mul(s: set<int>): int {
  if s == {} then 1 else
    var x :| x in s;  // this line takes the place of a call to Pick
    x * Mul(s - {x})
}

lemma MulMyWay(s: set<int>, y: int)
  requires y in s
  ensures Mul(s) == y * Mul(s - {y})
{
  var x :| x in s && Mul(s) == x * Mul(s - {x});  // this line takes the place of a call to Pick
  if y == x  {  // error: postcondition might not hold on this path
  } else {
    calc {
      Mul(s);
    ==  // def. Mul        // error: this step might not hold
      x * Mul(s - {x});
    ==  { MulMyWay(s - {x}, y); }
      x * y * Mul(s - {x} - {y});
    ==  { assert s - {x} - {y} == s - {y} - {x}; }
      y * x * Mul(s - {y} - {x});
    ==  { MulMyWay(s - {y}, x); }
      y * Mul(s - {y});
    }
  }
}

endlessly spins and never verifies... I thought it was related to multiplication but since Mul verifies, it must be related to properties of multisets.

function Prod(s: multiset<int>): int {
  if s == multiset{} then 1 else
    var x :| x in s;
    x * Prod(s - multiset{x})
}

lemma ProdMyWay(s: multiset<int>, y: int)
  requires y in s
  decreases s
  ensures Prod(s) == y * Prod(s - multiset{y})
{
  var x :| x in s && Prod(s) == x * Prod(s - multiset{x});
  if y == x  { 
  } else {
    assert s == (s - multiset{x}) + multiset{x};
    assert s == (s - multiset{x}- multiset{y}) + multiset{x}  + multiset{x}; 
    calc {
      Prod(s);
    ==  
      x * Prod(s - multiset{x});
    ==  { ProdMyWay(s - multiset{x}, y); }
      x * y * Prod(s - multiset{x} - multiset{y});
    ==  { assert s - multiset{x} - multiset{y} == s - multiset{y} - multiset{x}; }
      y * x * Prod(s - multiset{y} - multiset{x});
    ==  { ProdMyWay(s - multiset{y}, x); }
      y * Prod(s - multiset{y});
    }
  }
}

I think you have a typo in your file. You are trying to prove

assert s == (s - multiset{x}- multiset{y}) + multiset{x}  + multiset{x}; 

but what you probably want is

assert s == (s - multiset{x}- multiset{y}) + multiset{x}  + multiset{y}; 

Second, Dafny and SMT solvers have a hard time with non-linearity. You can either remove the non-linear axioms and invoke them manually, or give Dafny more hints about each individual assertion.

calc {
      Prod(s);
    ==  
      x * Prod(s - multiset{x});
    ==  { ProdMyWay(s - multiset{x}, y); }
      x * (y * Prod((s - multiset{x}) - multiset{y}));
    ==
      (x * y) * Prod((s - multiset{x}) - multiset{y});
    ==
      (y * x) * Prod((s - multiset{x}) - multiset{y});
    ==  { assert s - multiset{x} - multiset{y} == s - multiset{y} - multiset{x}; }
      (y * x) * Prod((s - multiset{y}) - multiset{x});
    ==
      y * (x * Prod((s - multiset{y}) - multiset{x}));
    ==  { ProdMyWay(s - multiset{y}, x); }
      y * Prod(s - multiset{y});
    }