Folding polynomial deg x

@[simp]theorem folding_polynomial_deg_x {q f : F[X]} :  degreeX (foldingPolynomial q f) = f.natDegree / q.natDegree := by    by_cases h: q.degree ≤ 0    · rw [Polynomial.degree_le_zero_iff] at h      rw [h, folding_polynomial_deg_x_C_q]      simp only [natDegree_C, Nat.div_zero]    · simp only [not_le] at h      induction n : f.natDegree using Nat.strong_induction_on generalizing f q with      | h n ih =>      by_cases h₁ : f.degree < q.degree ∨ f.degree ≤ 0 ∨ q.degree ≤ 0      · have h_deg_zero : degreeX (foldingPolynomial q f) = 0 :=          folding_polynomial_deg_x_base h₁        have h_deg_zero : f.natDegree < q.natDegree := by          by_cases hf : f = 0            <;> by_cases hq : q = 0            <;> simp_all +decide [Polynomial.degree_eq_natDegree]          aesop        rw [Nat.div_eq_of_lt] <;> aesop      · have h_deg :          degreeX (foldingPolynomial q f) = 1 + degreeX (foldingPolynomial q (f / q)) := by          apply folding_polynomial_deg_x_ind          · exact le_of_not_gt fun h₂ ↦ h₁ <| Or.inl h₂          · exact h        have h_deg_f_div_q : (f / q).natDegree = f.natDegree - q.natDegree := by          rw [Polynomial.div_def]          rw [Polynomial.natDegree_C_mul, Polynomial.natDegree_divByMonic]          · rw [Polynomial.natDegree_mul'] <;> aesop          · exact Polynomial.monic_mul_leadingCoeff_inv (Polynomial.ne_zero_of_degree_gt h)          · aesop        rw [h_deg, ih _ _ h h_deg_f_div_q]        · rw [←n, Nat.add_comm]          rw [            ←Nat.sub_add_cancel (show q.natDegree ≤ f.natDegree from ?_),            Nat.add_div]            <;> norm_num [Polynomial.natDegree_pos_iff_degree_pos.mpr h]          · exact Nat.mod_lt _ (Polynomial.natDegree_pos_iff_degree_pos.mpr h)          · exact              Polynomial.natDegree_le_natDegree                (le_of_not_gt fun h' ↦                    h₁ <| Or.inl                      <| by rw [                        Polynomial.degree_eq_natDegree,                        Polynomial.degree_eq_natDegree] at * <;> aesop)        · rw [←n]          exact Nat.sub_lt            (Polynomial.natDegree_pos_iff_degree_pos.mpr                (lt_of_not_ge fun h ↦ h₁                  <| Or.inr <| Or.inl h))            (Polynomial.natDegree_pos_iff_degree_pos.mpr h)