feat(data/polynomial): Add polynomial/eval lemmas (#3876)
Add some lemmas about `polynomial`. In particular, add lemmas about
`eval2` for the case that the ring `S` that we evaluate into is
non-commutative.
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
