proposition: Lemma poly_mul_cst_compat : forall v p var, eval var (poly_mul_cst v p) = andb v (eval var p).
proof: Proof. intros v p; induction p; intros var; simpl; [ring|]. case_decide; simpl; try_rewrite; [ring_simplify|ring]. replace (v && list_nth p2 var false && eval var p3) with (list_nth p2 var false && (v && eval var p3)) by ring. rewrite <- IHp2; inversion H; simpl; ring. Qed.
imports: Bool PArith DecidableClass Ring Lia