proposition: Fact ZM_correct_Z (vm : list Z) (e1 e2 : AGExpr) : all (Z.eqb 0) (ZMnorm (AGAdd e1 (AGOpp e2))) = true -> AGeval Z0 Z.opp Z.add vm e1 = AGeval Z0 Z.opp Z.add vm e2.
proof: Proof. now apply (ZM_correct _ _ _ Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l). Qed.
imports: Coq(ZArith)