mathlib3

08af4a31 - chore(data/polynomial/cancel_leads): golf using `compute_degree_le` (#14776)

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.