:: deftheorem defines Lucas_input NOMIN_9:def 9 :
for x0, y0, p0, q0 being Integer
for n0 being Nat holds Lucas_input (x0,y0,p0,q0,n0) = <*0,1,n0,x0,y0,x0,p0,q0,0,0*>;