fact: Definition copy_mset n (l: mset T): mset T := match n with | xH => l | _ => nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)