feat(data/polynomial/erase_lead + data/polynomial/reverse): rename an old lemma, add a stronger one (#12909)

Taking advantage of nat-subtraction in edge cases, a lemma that previously proved `x ≤ y` actually holds with `x ≤ y - 1`.

Thus, I renamed the old lemma to `original_name_aux` and `original_name` is now the name of the new lemma.  Since this lemma was used in a different file, I used the `_aux` name in the other file.

Note that the `_aux` lemma is currently an ingredient in the proof of the stronger lemma.  It may be possible to have a simple direct proof of the stronger one that avoids using the `_aux` lemma, but I have not given this any thought.

Author: adomani

src/data/polynomial/erase_lead.lean

@@ -134,12 +134,12 @@ begin
   apply coeff_eq_zero_of_degree_lt hi
 end
 
-lemma erase_lead_nat_degree_le : (erase_lead f).nat_degree ≤ f.nat_degree :=
+lemma erase_lead_nat_degree_le_aux : (erase_lead f).nat_degree ≤ f.nat_degree :=
 nat_degree_le_nat_degree erase_lead_degree_le
 
 lemma erase_lead_nat_degree_lt (f0 : 2 ≤ f.support.card) :
   (erase_lead f).nat_degree < f.nat_degree :=
-lt_of_le_of_ne erase_lead_nat_degree_le $ ne_nat_degree_of_mem_erase_lead_support $
+lt_of_le_of_ne erase_lead_nat_degree_le_aux $ ne_nat_degree_of_mem_erase_lead_support $
   nat_degree_mem_support_of_nonzero $ erase_lead_ne_zero f0
 
 lemma erase_lead_nat_degree_lt_or_erase_lead_eq_zero (f : R[X]) :
@@ -153,6 +153,13 @@ begin
     apply erase_lead_nat_degree_lt (lt_of_not_ge h) }
 end
 
+lemma erase_lead_nat_degree_le (f : R[X]) : (erase_lead f).nat_degree ≤ f.nat_degree - 1 :=
+begin
+  rcases f.erase_lead_nat_degree_lt_or_erase_lead_eq_zero with h | h,
+  { exact nat.le_pred_of_lt h },
+  { simp only [h, nat_degree_zero, zero_le] }
+end
+
 end erase_lead
 
 /-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
@@ -188,7 +195,7 @@ begin
         rintro rfl,
         simpa using f0 } },
     { exact (nat_degree_C_mul_X_pow_le f.leading_coeff f.nat_degree).trans df },
-    { exact hc _ (erase_lead_nat_degree_le.trans df) (erase_lead_card_support f0) },
+    { exact hc _ (erase_lead_nat_degree_le_aux.trans df) (erase_lead_card_support f0) },
     { refine P_C_mul_pow _ _ _ df,
       rw [ne.def, leading_coeff_eq_zero, ← card_support_eq_zero, f0],
       exact nat.succ_ne_zero _ } }

src/data/polynomial/reverse.lean

@@ -162,7 +162,7 @@ begin
       { exact le_add_left card_support_C_mul_X_pow_le_one },
       { exact (le_trans (nat_degree_C_mul_X_pow_le g.leading_coeff g.nat_degree) Og) },
       { exact nat.lt_succ_iff.mp (gt_of_ge_of_gt Cg (erase_lead_support_card_lt g0)) },
-      { exact le_trans erase_lead_nat_degree_le Og } } },
+      { exact le_trans erase_lead_nat_degree_le_aux Og } } },
   --first induction (left): induction step
   { intros N O f g Cf Cg Nf Og,
     by_cases f0 : f = 0,
@@ -173,7 +173,7 @@ begin
     { exact le_add_left card_support_C_mul_X_pow_le_one },
     { exact (le_trans (nat_degree_C_mul_X_pow_le f.leading_coeff f.nat_degree) Nf) },
     { exact nat.lt_succ_iff.mp (gt_of_ge_of_gt Cf (erase_lead_support_card_lt f0)) },
-    { exact (le_trans erase_lead_nat_degree_le Nf) } },
+    { exact (le_trans erase_lead_nat_degree_le_aux Nf) } }
 end
 
 @[simp] theorem reflect_mul