theorem lemlowp0: :: REALALG1:7

for R being Ring
for p being Polynomial of R holds min* { i where i is Nat : (p + (0_. R)) . i <> 0. R } = min* { i where i is Nat : p . i <> 0. R }