proposition: Lemma copy_idem i (Idem : Idempotent R (Bin.value (e_bin i))) n x : copy (plus:=(Bin.value (e_bin i))) n x == x.
proof: Proof. induction n using Pos.peano_ind; simpl. - apply copy_xH. - rewrite copy_Psucc, IHn; apply law_idem. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)