proposition: Lemma is_reduced_compat_neg : forall {n} {b1} (p1 : poly b1 n) (Hp1 : is_reduced p1), is_reduced (poly_neg p1).
proof: Proof. intros. depind Hp1; try destruct z, i; autorewrite with poly_neg; try constructor; auto. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef