fact: Fixpoint copy' n x := match n with | xH => x | xI n => let xn := copy' n x in plus (plus xn xn) x | xO n => let xn := copy' n x in (plus xn xn) end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)