proposition: Lemma neg_eval : forall {n} {b1} (p1 : poly b1 n) v, (- eval p1 v)%Z = eval (poly_neg p1) v.
proof: Proof. Ltac XX := (autorewrite with poly_neg plus eval; auto with zarith). depind p1; depelim v; XX. destruct z; depelim i; XX. rewrite <- IHp1_1; rewrite <- IHp1_2; nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef