proposition: Lemma copy_mset' n (l: mset T) : copy_mset n l = nelist_map (fun vm => let '(v,m):=vm in (v,Pmult n m)) l.
proof: Proof. unfold copy_mset. destruct n; try reflexivity. simpl. induction l as [|[a l] IHl]; simpl; try congruence. destruct a; reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)