proposition: Lemma plus_eval : forall {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 n) v, (eval p1 v + eval p2 v)%Z = eval (plus p1 p2).2 v.
proof: Proof. Proof with (simp plus eval; auto with zarith). Ltac X := (simp plus eval; auto with zarith). intros until p2. let f := constr:(fun_elim (f:=@plus)) in apply f; intros; depelim v; X; try rewrite <- H; X. - rewrite Heq in Hind. specialize (Hind (Vector.cons h v)). rewrite poly_z_eval in Hind. nia. - rewrite Heq in Hind. rewrite <- Hind. nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef