theorem lem4: :: LAGRA4SQ:4

for p being odd Prime
for s being Nat
for j1, j2 being Integer st 2 * s = p + 1 & j1 in rng (LAG4SQf s) & j2 in rng (LAG4SQf s) & not j1 = j2 holds
j1 mod p <> j2 mod p