let m, n be non zero Nat; :: thesis: ( m is_quadratic_residue_mod n implies ex i being Nat st (ArProg (m,n)) . i is square )
assume m is_quadratic_residue_mod n ; :: thesis: ex i being Nat st (ArProg (m,n)) . i is square
then consider xx being Integer such that
B1: ((xx ^2) - m) mod n = 0 by INT_5:def 2;
reconsider x = |.xx.| as Nat ;
x ^2 = xx ^2 by COMPLEX1:75;
then n divides (x ^2) - m by B1, INT_1:62;
then consider ii being Integer such that
B3: (x ^2) - m = ii * n ;
B4: (ii * n) + m = x ^2 by B3;

per cases ( ii >= 0 or ii < 0 ) ;

suppose ii >= 0 ; :: thesis: ex i being Nat st (ArProg (m,n)) . i is square

then ii in NAT by INT_1:3;
then reconsider ii = ii as Nat ;
take i = ii; :: thesis: (ArProg (m,n)) . i is square
thus (ArProg (m,n)) . i is square by B4, NUMBER06:7; :: thesis: verum

end;

suppose DD: ii < 0 ; :: thesis: ex i being Nat st (ArProg (m,n)) . i is square

then - ii in NAT by INT_1:3;
then reconsider mm = - ii as Nat ;
set b = m;
set a = n;
set k = ii;
So: ((mm * n) + x) ^2 = ((n * ((mm ^2) * n)) + (((n * 2) * mm) * x)) + (x ^2)
.= (n * ((((mm ^2) * n) + ((2 * mm) * x)) + ii)) + m by B3 ;
(mm * n) + (2 * x) >= 1 + 0 by DD, NAT_1:13;
then mm * ((mm * n) + (2 * x)) >= 1 * (- ii) by XREAL_1:64;
then (mm * ((mm * n) + (2 * x))) + ii >= (- ii) + ii by XREAL_1:6;
then (mm * ((mm * n) + (2 * x))) + ii >= 0 ;
then reconsider wa = (((mm ^2) * n) + ((2 * mm) * x)) + ii as Nat ;
take wa ; :: thesis: (ArProg (m,n)) . wa is square
thus (ArProg (m,n)) . wa is square by NUMBER06:7, So; :: thesis: verum

end;

end;