lemmas): three lemmas on nat_degrees, bits and neg (#15522)

Commit

3 years ago

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`.

Author

adomani

Parents

35639363

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

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