proposition: Lemma copy_mset_succ n (l: mset T) : eval (sum i (copy_mset (Pos.succ n) l)) == @Bin.value _ _ (e_bin i) (eval (sum i l)) (eval (sum i (copy_mset n l))).
proof: Proof. rewrite 2 copy_mset'. induction l as [[a m]|[a m] l IHl]. simpl eval. rewrite <- copy_plus; auto. rewrite Pmult_Sn_m. reflexivity. simpl nelist_map. rewrite ! eval_sum_cons. rewrite IHl. clear IHl. rewrite Pmult_Sn_m. rewrite copy_plus; auto. rewrite <- !law_assoc. apply Binvalue_Proper; try reflexivity. rewrite law_comm . rewrite <- !law_assoc. apply proper; try reflexivity. apply law_comm. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)