proposition: Lemma copy_Psucc : forall n x, R (copy (Pos.succ n) x) (plus x (copy n x)).
proof: Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)