Eq zero of folding polynomial eq zero

lemma eq_zero_of_folding_polynomial_eq_zero {q f : F[X]}  (h : foldingPolynomial q f = 0) : f = 0 := by    induction n : f.natDegree using Nat.strong_induction_on generalizing f with    | h n' ih =>      by_cases h₁ :      f.degree < q.degree        ∨ f.degree ≤ 0        ∨ q.degree ≤ 0 <;> simp_all only [ext_iff, coeff_zero, not_or, not_lt, not_le]      · rw [folding_polynomial_def_base_case h₁] at h        intro n        specialize h n 0        aesop      · have h_rem_zero : f % q = 0 := by          rw [folding_polynomial_def_ind_case h₁.1 h₁.2.2] at h          ext n          specialize h n 0          simp_all +decide [Polynomial.coeff_map]        have h_quot_zero : f / q = 0 := by          have h_quot_zero : foldingPolynomial q (f / q) = 0 := by            have h_quot_zero :            foldingPolynomial q f              = (Polynomial.map Polynomial.C (f % q))                + Polynomial.C Polynomial.X                    * foldingPolynomial q (f / q) := by              rw [folding_polynomial_def_ind_case] <;> aesop            simp_all +decide only [Polynomial.map_zero, zero_add, coeff_C_mul,            EuclideanDomain.mod_eq_zero, ext_iff, coeff_add, coeff_map, add_zero, coeff_zero]            intro n n_1            specialize h n (n_1 + 1)            simp_all +decide          contrapose! ih          refine            ⟨Polynomial.natDegree (f / q),            by {              have h_deg_f : f.natDegree = q.natDegree + (f / q).natDegree := by                rw [←Polynomial.natDegree_mul']                · rw [EuclideanDomain.mul_div_cancel'] <;> aesop                · aesop              linarith [                Polynomial.natDegree_pos_iff_degree_pos.mpr h₁.2.1,                Polynomial.natDegree_pos_iff_degree_pos.mpr h₁.2.2]            },            f / q,            by simp_all +decide,            rfl,            Polynomial.natDegree (f / q), by simp [ih]⟩        rw [EuclideanDomain.mod_eq_sub_mul_div] at h_rem_zero        aesop