let a be Integer; :: thesis: for p being Prime st p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p holds
ex x, y being Integer st
( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p )
let p be Prime; :: thesis: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p implies ex x, y being Integer st
( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p ) )
assume A1: ( p > 2 & a gcd p = 1 & a is_quadratic_residue_mod p ) ; :: thesis: ex x, y being Integer st
( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p )
then consider x being Integer such that
A2: ((x ^2 ) - a) mod p = 0 by Def2;
A3: not x, - x are_congruent_mod p

proof

assume x, - x are_congruent_mod p ; :: thesis: contradiction
then p divides x - (- x) by INT_2:19;
then A4: p divides 2 * x ;
2,p are_relative_prime by A1, INT_2:44, INT_2:47;
then 2 gcd p = 1 by INT_2:def 4;
then p divides x by A4, WSIERP_1:36;
then consider i being Integer such that
A5: x = p * i by INT_1:def 9;
x <> 0

proof

assume x = 0 ; :: thesis: contradiction
then p divides - a by A2, INT_1:89;
then p divides a * 1 by INT_2:14;
then p <= 1 by A1, NAT_D:7, WSIERP_1:36;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

then A6: i <> 0 by A5;
x gcd p = (p * i) gcd (p * 1) by A5
.= p * (i gcd 1) by A6, EULER_1:16
.= p * 1 by WSIERP_1:13 ;
then x gcd p <> 1 by INT_2:def 5;
then not x,p are_relative_prime by INT_2:def 4;
hence contradiction by A1, A2, Th14; :: thesis: verum

end;

take x ; :: thesis: ex y being Integer st
( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p )
take y = - x; :: thesis: ( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p )
thus ( ((x ^2 ) - a) mod p = 0 & ((y ^2 ) - a) mod p = 0 & not x,y are_congruent_mod p ) by A2, A3; :: thesis: verum