proposition: Lemma poly_nz {n} (p : poly false n) : exists m, IsNZ (get_coef m p).
proof: Proof. Proof with (autorewrite with get_coef; auto). intros. depind p. exists mono_z... destruct IHp. exists (mono_l x)... destruct IHp2. exists (mono_s x)... Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef