proposition: Lemma poly_mul_compat : forall pl pr var, eval var (poly_mul pl pr) = andb (eval var pl) (eval var pr).
proof: Proof. intros pl; induction pl; intros pr var; simpl. - apply poly_mul_cst_compat. - case_decide; simpl. + rewrite IHpl1; ring_simplify. replace (eval var pr && list_nth p var false && eval var pl2) with (list_nth p var false && (eval var pl2 && eval var pr)) by ring. now rewrite <- IHpl2; inversion H; simpl; ring. + rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring. Qed.
imports: Bool PArith DecidableClass Ring Lia