multiset_simplify_singletons fails due to unification nonsense

I'd like to use multiset_solver here but it doesn't work. The problem turns out to be that multiset_simplify_singletons doesn't make progress when it should. Specifically, rewrite multiplicity_singleton fails on multiplicity x {[+ x +]} ≤ 0. This is Coq's rewrite -- ssreflect rewrite works fine in the same situation.