proposition: Lemma poly_l_or_s_eval : forall {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 (S n)) h v, eval (poly_l_or_s p1 p2).2 (Vector.cons h v) = (eval p1 v + h * eval p2 (Vector.cons h v))%Z.
proof: Proof. intros. funelim (poly_l_or_s p1 p2); simp eval; trivial. rewrite poly_z_eval. nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef