proposition: Lemma poly_nz_eval : forall {n}, (forall (p : poly false n), exists v, IsNZ (eval p v)) /\ (forall (p : poly false (S n)), exists v, forall m, exists x, IsNZ x /\ (Z.abs (x * eval p (Vector.cons x v)) > Z.abs m)%Z).
proof: Proof. Proof with (autorewrite with eval; auto using poly_nz_eval'). depind n; match goal with | [ |- ?P /\ ?Q ] => assert (HP : P); [|split;[auto|]] end... depelim p; exists Vector.nil... - destruct IHn as [IHn1 IHn2]; depelim p. + destruct (IHn1 p) as [v Hv]; exists (Vector.cons 0%Z v)... + destruct (IHn2 p2) as [v Hv]. destruct (Hv (eval p1 v)) as [x [_ Hx]]. exists (Vector.cons x v)... rewrite IsNZ_spec; nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef