proposition: Lemma poly_z_eval {n} (p : poly true n) v : eval p v = 0%Z.
proof: Proof. funelim (eval p v); [ reflexivity | assumption ]. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef