Folding polynomial deg y bound

theorem folding_polynomial_deg_y_bound {q f : F[X]} (h : 0 < q.degree) :   natDegreeY (foldingPolynomial q f) < q.degree := by  simp only [natDegreeY, coe_lt_degree]  induction n : f.natDegree using Nat.strong_induction_on generalizing f q with  | h n ih =>  by_cases hq : f.degree < q.degree  · have h_folding_eq_map : foldingPolynomial q f = Polynomial.map Polynomial.C f :=      folding_polynomial_eq_map_of_f_degree_lt_q_degree hq    by_cases hf : f = 0      <;> simp_all only [natDegree_map, natDegree_zero, degree_zero, foldingPolynomial_zero,        Polynomial.map_zero, gt_iff_lt]    · exact n.symm ▸ Polynomial.natDegree_pos_iff_degree_pos.mpr h    · rw [←n, Polynomial.degree_eq_natDegree hf] at *      aesop  · have h_fold :      foldingPolynomial q f =        (Polynomial.map Polynomial.C (f % q)) +          Polynomial.C Polynomial.X *            (foldingPolynomial q (f / q)) := by      rw [folding_polynomial_def_ind_case]      · simp only [not_lt] at hq        exact hq      · exact h    refine h_fold ▸ lt_of_le_of_lt (Polynomial.natDegree_add_le _ _) (max_lt (by {      have h_deg_mod : (f % q).degree < q.degree :=        EuclideanDomain.mod_lt f (Polynomial.ne_zero_of_degree_gt h)      by_cases h : f % q = 0 <;> simp_all +decide only [not_lt, Polynomial.map_zero, zero_add,        degree_zero, EuclideanDomain.mod_eq_zero, natDegree_map, gt_iff_lt]      · rw [EuclideanDomain.mod_eq_zero.mpr h]        simp +decide [Polynomial.natDegree_pos_iff_degree_pos.mpr ‹_›]      · exact Polynomial.natDegree_lt_natDegree (by aesop) h_deg_mod    }) (by {      apply lt_of_le_of_lt (Polynomial.natDegree_C_mul_le _ _)      apply ih _ _ h rfl      rw [←n, Polynomial.div_def]      rw [        Polynomial.natDegree_C_mul,        Polynomial.natDegree_divByMonic]          <;> norm_num [            Polynomial.natDegree_mul',            Polynomial.natDegree_C, show q ≠ 0 by aesop]      · simp only [not_lt] at hq        exact          ⟨Polynomial.natDegree_pos_iff_degree_pos.mpr            (lt_of_lt_of_le h hq),            Polynomial.natDegree_pos_iff_degree_pos.mpr h⟩      · exact Polynomial.monic_mul_leadingCoeff_inv (by aesop)    }))