theorem :: POLYNOM3:23

for L being non empty ZeroStr
for p being Polynomial of L
for n being Nat holds
( n >= len p iff n is_at_least_length_of p ) by ALGSEQ_1:8, XXREAL_0:2, ALGSEQ_1:def 3;