proposition: Lemma mset_compare_weak_spec: forall h k, compare_weak_spec h k (mset_compare compare h k).
proof: Proof. apply list_compare_weak_spec. intros [u n] [v m]. case (Hcompare u v); try constructor. case (pos_compare_weak_spec n m); try constructor. Defined.
imports: Coq(Arith NArith List RelationClasses)