feat(data/polynomial/degree/lemmas): three lemmas on nat_degrees, bits and neg (#15522)
feat(data/polynomial/degree/lemmas): three lemmas on nat_degrees, bits and neg (#15522)

These three lemmas are used in #14762, to help the tactic `compute_degree_le`.






leanprover-community/mathlib,leanprover-community/mathlib