fact: Definition mset_compare A B compare: mset A -> mset B -> comparison := list_compare (fun un vm => let '(u,n) := un in let '(v,m) := vm in lex (compare u v) (pos_compare n m)).
imports: Coq(Arith NArith List RelationClasses)