proposition: Theorem poly_eval_eq : forall {n} {b1} (p1 : poly b1 n) {b2} (p2 : poly b2 n), (forall v, eval p1 v = eval p2 v) -> (b1 ; p1) = (b2; p2) :> { b : bool & poly b n}.
proof: Proof. intros. remember (plus p1 (poly_neg p2)) as P; destruct P as [b P]; destruct b. - apply poly_diff_z_eq; inversion HeqP; auto. - exfalso. destruct (@poly_nz_eval n) as [H0 _]; destruct (H0 P) as [v H1]. assert (eval P v = eval (plus p1 (poly_neg p2)).2 v); [inversion HeqP; auto|]. rewrite H2 in H1; autorewrite with eval in H1; rewrite (H v) in H1. rewrite IsNZ_spec in H1. nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef