proposition: Lemma one_eval : forall n v, 1%Z = eval (@poly_one n) v.
proof: Proof. depind n; depelim v; intros; simpl; autorewrite with eval; auto. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef