let D be Nat; :: thesis: for p1, p2 being Pell's_solution of D st 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square holds
( p1 `1 < p2 `1 & p1 `2 < p2 `2 )
let p1, p2 be Pell's_solution of D; :: thesis: ( 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square implies ( p1 `1 < p2 `1 & p1 `2 < p2 `2 ) )
assume A1: ( 1 < (p1 `1) + ((p1 `2) * (sqrt D)) & (p1 `1) + ((p1 `2) * (sqrt D)) < (p2 `1) + ((p2 `2) * (sqrt D)) & not D is square & ( p1 `1 >= p2 `1 or p1 `2 >= p2 `2 ) ) ; :: thesis: contradiction

per cases ( p1 `2 >= p2 `2 or p1 `1 >= p2 `1 ) by A1;

suppose A2: p1 `2 >= p2 `2 ; :: thesis: contradiction

A3: sqrt D > 0 by A1, SQUARE_1:25;
A4: p1 is positive by Th18, A1;
(p2 `1) + ((p2 `2) * (sqrt D)) > 1 by A1, XXREAL_0:2;
then A5: p2 is positive by Th18, A1;
(((p1 `1) ^2) - (((p1 `2) ^2) * D)) + (((p1 `2) ^2) * D) = 1 + (((p1 `2) ^2) * D) by Def1;
then A6: p1 `1 = sqrt (1 + (((p1 `2) ^2) * D)) by SQUARE_1:def 2, A4;
(((p2 `1) ^2) - (((p2 `2) ^2) * D)) + (((p2 `2) ^2) * D) = 1 + (((p2 `2) ^2) * D) by Def1;
then A7: p2 `1 = sqrt (1 + (((p2 `2) ^2) * D)) by SQUARE_1:def 2, A5;
(p1 `2) ^2 >= (p2 `2) ^2 by SQUARE_1:15, A5, A2;
then ((p1 `2) ^2) * D >= ((p2 `2) ^2) * D by XREAL_1:64;
then (((p1 `2) ^2) * D) + 1 >= (((p2 `2) ^2) * D) + 1 by XREAL_1:6;
then A8: p1 `1 >= p2 `1 by A6, A7, SQUARE_1:26;
(p1 `2) * (sqrt D) >= (p2 `2) * (sqrt D) by A2, XREAL_1:64, A3;
hence contradiction by A1, A8, XREAL_1:7; :: thesis: verum

end;

suppose A9: p1 `1 >= p2 `1 ; :: thesis: contradiction

A10: sqrt D > 0 by A1, SQUARE_1:25;
A11: p1 is positive by Th18, A1;
(p2 `1) + ((p2 `2) * (sqrt D)) > 1 by A1, XXREAL_0:2;
then A12: p2 is positive by Th18, A1;
A13: (((p1 `1) ^2) - (((p1 `2) ^2) * D)) + (((p1 `2) ^2) * D) = 1 + (((p1 `2) ^2) * D) by Def1;
A14: p1 `1 = sqrt (1 + (((p1 `2) ^2) * D)) by A13, SQUARE_1:def 2, A11;
A15: (((p2 `1) ^2) - (((p2 `2) ^2) * D)) + (((p2 `2) ^2) * D) = 1 + (((p2 `2) ^2) * D) by Def1;
A16: p2 `1 = sqrt (1 + (((p2 `2) ^2) * D)) by A15, SQUARE_1:def 2, A12;
( sqrt (1 + (((p1 `2) ^2) * D)) >= 0 & sqrt (1 + (((p2 `2) ^2) * D)) >= 0 ) by SQUARE_1:25;
then A17: (sqrt (1 + (((p1 `2) ^2) * D))) ^2 >= (sqrt (1 + (((p2 `2) ^2) * D))) ^2 by SQUARE_1:15, A9, A14, A16;
(sqrt (1 + (((p2 `2) ^2) * D))) * (sqrt (1 + (((p2 `2) ^2) * D))) = sqrt ((1 + (((p2 `2) ^2) * D)) * (1 + (((p2 `2) ^2) * D))) by SQUARE_1:29;
then A18: sqrt ((1 + (((p1 `2) ^2) * D)) ^2) >= sqrt ((1 + (((p2 `2) ^2) * D)) ^2) by A17, SQUARE_1:29;
A19: sqrt ((1 + (((p1 `2) ^2) * D)) ^2) = 1 + (((p1 `2) ^2) * D) by SQUARE_1:22;
sqrt ((1 + (((p2 `2) ^2) * D)) ^2) = 1 + (((p2 `2) ^2) * D) by SQUARE_1:22;
then (1 + (((p1 `2) ^2) * D)) - 1 >= (1 + (((p2 `2) ^2) * D)) - 1 by XREAL_1:13, A18, A19;
then A20: (((p1 `2) ^2) * D) / D >= (((p2 `2) ^2) * D) / D by XREAL_1:72;
A21: (((p1 `2) ^2) * D) / D = (p1 `2) ^2 by XCMPLX_1:89, A1;
(((p2 `2) ^2) * D) / D = (p2 `2) ^2 by XCMPLX_1:89, A1;
then A22: sqrt ((p1 `2) ^2) >= sqrt ((p2 `2) ^2) by SQUARE_1:26, A20, A21;
sqrt ((p2 `2) ^2) = p2 `2 by SQUARE_1:22, A12;
then A23: p1 `2 >= p2 `2 by A22, SQUARE_1:22, A11;
(p1 `2) * (sqrt D) >= (p2 `2) * (sqrt D) by A23, XREAL_1:64, A10;
hence contradiction by A1, A9, XREAL_1:7; :: thesis: verum

end;

end;