feat(data/polynomial): simp lemmas for bit0 / bit1 (#3376)
Add lemmas on polynomials and bit0/bit1 (as suggested [here](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Eval.20of.20constant.20polynomial))
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
