proposition: Lemma ZM_norm_subst (vm : list G) (e : AGExpr) : ZMsubst vm (ZMnorm e) = AGeval vm e.
proof: Proof. induction e as [j| |e IHe|e1 IHe1 e2 IHe2]; simpl; trivial. - revert vm; induction j as [|j IHj]; destruct vm as [|v vm]; simpl; trivial. + now rewrite add0x, addx0. + now rewrite add0x, IHj. - rewrite <- IHe; clear IHe; revert vm. induction (ZMnorm e) as [|x xs IHxs]; destruct vm as [|v vm]; simpl; try now rewrite opp0. rewrite IHxs, oppD; f_equal. now destruct x; simpl; [rewrite opp0| |rewrite oppK]. - rewrite <- IHe1, <- IHe2; clear IHe1 IHe2; revert vm. generalize (ZMnorm e1) as xs, (ZMnorm e2) as ys; induction xs as [|x xs IHxs]; destruct ys as [|y ys]; destruct vm as [|v vm]; simpl; try now (rewrite add0x || rewrite addx0). now rewrite addACA, <-IHxs, mulzDl. Qed.
imports: Coq(ZArith)