fact: Fixpoint ZMnorm (e : AGExpr) : list Z := match e with | AGX j => ncons j 0%Z (cons 1%Z nil) | AGO => nil | AGOpp e1 => List.map Z.opp (ZMnorm e1) | AGAdd e1 e2 => (fix add_rec (xs ys : list Z) : list Z := match xs, ys with | nil, s | s, nil => s | cons x xs, cons y ys => cons (Z.add x y) (add_rec xs ys) end) (ZMnorm e1) (ZMnorm e2) end.
imports: Coq(ZArith)