proposition: Lemma copy_mset_copy : forall n (m : mset T), eval (sum i (copy_mset n m)) == @copy _ (@Bin.value _ _ (e_bin i)) n (eval (sum i m)).
proof: Proof. induction n using Pind; intros. - unfold copy_mset. rewrite copy_xH. reflexivity. - rewrite copy_mset_succ. rewrite copy_Psucc. rewrite IHn. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)