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