Commit 2022-01-08 16:29 56f021a9

feat(data/polynomial/{erase_lead + denoms_clearable}): strengthen a lemma (#11257) This PR is a step in the direction of simplifying #11139 . It strengthens lemma induction_with_nat_degree_le by showing that restriction can be strengthened on one of the assumptions. It proves a lemma computing the nat_degree under functions on polynomials that include the shift of a variable. EDIT: the lemma was moved to the later PR #11265. It fixes the unique use of lemma induction_with_nat_degree_le. Zulip discussion