feat: add theorem natDegree_modByMonic_lt (#7278)

Adds the natDegree analogue of this theorem

Co-authored-by: Pratyush Mishra <prat@upenn.edu>

Mathlib/Data/Polynomial/Div.lean

@@ -164,6 +164,15 @@ theorem degree_modByMonic_lt [Nontrivial R] :
   termination_by degree_modByMonic_lt p q hq => p
 #align polynomial.degree_mod_by_monic_lt Polynomial.degree_modByMonic_lt
 
+theorem natDegree_modByMonic_lt (p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q ≠ 1) :
+    natDegree (p %ₘ q) < q.natDegree := by
+  by_cases hpq : p %ₘ q = 0
+  · rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]
+    contrapose! hq
+    exact eq_one_of_monic_natDegree_zero hmq hq
+  · haveI := Nontrivial.of_polynomial_ne hpq
+    exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)
+
 @[simp]
 theorem zero_modByMonic (p : R[X]) : 0 %ₘ p = 0 := by
   unfold modByMonic divModByMonicAux