Nat Degree sharing Polynomial le

theorem natDegree_sharingPolynomial_le (secretValue : F) (tail : _root_.Polynomial F) {n : ℕ}    (hdeg : tail.degree < n) :    (sharingPolynomial secretValue tail).natDegree ≤ n := by  rw [sharingPolynomial]  refine (_root_.Polynomial.natDegree_add_le _ _).trans ?_  rw [max_le_iff]  constructor  · rw [_root_.Polynomial.natDegree_C]    exact Nat.zero_le n  · by_cases htail : tail = 0    · simp [htail]    · rw [_root_.Polynomial.natDegree_X_mul htail]      have htailDegree : tail.natDegree < n := by        have := hdeg        rw [_root_.Polynomial.degree_eq_natDegree htail] at this        exact_mod_cast this      exact Nat.succ_le_of_lt htailDegree