proposition: Lemma poly_mul_mon_compat : forall i p var, eval var (poly_mul_mon i p) = (list_nth i var false && eval var p).
proof: Proof. intros i p var; induction p; simpl; case_decide; simpl; try_rewrite; try ring. inversion H; ring. Qed.
imports: Bool PArith DecidableClass Ring Lia