chore(data/polynomial/{degree/basic, eval}): Some trivial lemmas about polynomials (#4768)
I have added the lemma `supp_card_le_succ_nat_degree` about the cardinality of the support of a polynomial and removed the useless commutativity assumptio in `map_sum` and `map_neg`.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>