proposition: Lemma red_ok : forall {n} {b} (p : poly b n), is_reduced p -> (forall v, eval p (Vector.map (fun x : bool => if x then 1%Z else 0%Z) v) = 0%Z) -> b = true.
proof: Proof. intros n b p Hp H; depind Hp. - auto. - specialize (H Vector.nil); autorewrite with eval in H; destruct z, i; discriminate. - apply IHHp. intro v. specialize (H (Vector.cons false v)). autorewrite with eval in H. auto. - assert (b1 = true). + apply IHHp1. intro v. specialize (H (Vector.cons false v)). autorewrite with eval in H. simpl in H. rewrite Z.add_0_r in H. auto. + subst. apply IHHp2. intro v. specialize (H (Vector.cons true v)). simpl in H. autorewrite with eval in H. rewrite poly_z_eval in H. nia. Qed.
imports: Program.Basics Program.Tactics Equations(Equations) ZArith Lia Psatz Nat Coq.Vectors.VectorDef