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 (simp eval). depind p. - destruct (H p) as [v Hv]. exists v; intros; exists (1 + Z.abs m)%Z... rewrite IsNZ_spec in Hv |- *. nia. - destruct (IHp2 H) as [v Hv]; exists v; intros. destruct (Hv (Z.abs (eval p1 v) + Z.abs m)%Z) as [x [Hx0 Hx1]]; exists x... split; auto. rewrite IsNZ_spec in Hx0. nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef