Commit 2022-07-27 19:44 08af4a31

chore(data/polynomial/cancel_leads): golf using compute_degree_le (#14776) This PR is the companion to #14762. It serves to show how to use the tactic in a few cases in what is already in mathlib. I generalized lemma nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree to assume ring instead of comm_ring + is_domain. The lemma with the weaker assumptions is nat_degree_cancel_leads_lt_of_nat_degree_le_nat_degree_of_comm. I left the old lemma as well,with proof a simple application of the newer lemma.