feat(data/polynomial/degree/definitions): add degree_X_sub_C_le (#1…

…6404)

src/data/polynomial/algebra_map.lean

@@ -375,7 +375,7 @@ begin
   have bound := calc
     (p * (X - C r)).nat_degree
          ≤ p.nat_degree + (X - C r).nat_degree : nat_degree_mul_le
-     ... ≤ p.nat_degree + 1 : add_le_add_left nat_degree_X_sub_C_le _
+     ... ≤ p.nat_degree + 1 : add_le_add_left (nat_degree_X_sub_C_le _) _
      ... < p.nat_degree + 2 : lt_add_one _,
   rw sum_over_range' _ _ (p.nat_degree + 2) bound,
   swap,

src/data/polynomial/degree/definitions.lean

@@ -1047,10 +1047,11 @@ calc degree (p - q) = degree (erase (nat_degree q) p + -erase (nat_degree q) q)
   : degree_neg (erase (nat_degree q) q) ▸ degree_add_le _ _
 ... < degree p : max_lt_iff.2 ⟨hd' ▸ degree_erase_lt hp0, hd.symm ▸ degree_erase_lt hq0⟩
 
+lemma degree_X_sub_C_le (r : R) : (X - C r).degree ≤ 1 :=
+(degree_sub_le _ _).trans (max_le degree_X_le (degree_C_le.trans zero_le_one))
 
-lemma nat_degree_X_sub_C_le {r : R} : (X - C r).nat_degree ≤ 1 :=
-nat_degree_le_iff_degree_le.2 $ le_trans (degree_sub_le _ _) $ max_le degree_X_le $
-le_trans degree_C_le $ with_bot.coe_le_coe.2 zero_le_one
+lemma nat_degree_X_sub_C_le (r : R) : (X - C r).nat_degree ≤ 1 :=
+nat_degree_le_iff_degree_le.2 $ degree_X_sub_C_le r
 
 lemma degree_sub_eq_left_of_degree_lt (h : degree q < degree p) : degree (p - q) = degree p :=
 by { rw ← degree_neg q at h, rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h] }