Degree of the remainder of polynomial division

Stream: Is there code for X?

[Patrick Lutz]

Is there anything in mathlib saying that if p and q are polynomials (with q nonzero) then the degree of p % q is less than the degree of q? It seems like this must be in mathlib, but somehow I can only find it stated for monic polynomials (in data.polynomial.div).

[Heather Macbeth]

Is this docs#euclidean_domain.mod_lt ?

[Patrick Lutz]

Ohh, I think so! Thanks!