let i1, i2, j1, j2 be Nat; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & 1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) holds
(G1 * (i1,(j1 -' 1))) `2 <= (G2 * (i2,(j2 -' 1))) `2
let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & 1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 & 1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 & G1 * (i1,j1) = G2 * (i2,j2) implies (G1 * (i1,(j1 -' 1))) `2 <= (G2 * (i2,(j2 -' 1))) `2 )
assume that
A1: Values G1 c= Values G2 and
A2: ( 1 <= i1 & i1 <= len G1 ) and
A3: 1 < j1 and
A4: j1 <= width G1 and
A5: ( 1 <= i2 & i2 <= len G2 ) and
A6: 1 < j2 and
A7: j2 <= width G2 and
A8: G1 * (i1,j1) = G2 * (i2,j2) ; :: thesis: (G1 * (i1,(j1 -' 1))) `2 <= (G2 * (i2,(j2 -' 1))) `2
set p = G1 * (i1,(j1 -' 1));
A9: 1 <= j1 -' 1 by A3, NAT_D:49;
then A10: j1 -' 1 < j1 by NAT_D:51;
then j1 -' 1 < width G1 by A4, XXREAL_0:2;
then [i1,(j1 -' 1)] in Indices G1 by A2, A9, MATRIX_0:30;
then G1 * (i1,(j1 -' 1)) in { (G1 * (i,j)) where i, j is Nat : [i,j] in Indices G1 } ;
then G1 * (i1,(j1 -' 1)) in Values G1 by MATRIX_0:39;
then G1 * (i1,(j1 -' 1)) in Values G2 by A1;
then G1 * (i1,(j1 -' 1)) in { (G2 * (i,j)) where i, j is Nat : [i,j] in Indices G2 } by MATRIX_0:39;
then consider i, j being Nat such that
A11: G1 * (i1,(j1 -' 1)) = G2 * (i,j) and
A12: [i,j] in Indices G2 ;
A13: 1 <= j by A12, MATRIX_0:32;
A14: j <= width G2 by A12, MATRIX_0:32;
( 1 <= i & i <= len G2 ) by A12, MATRIX_0:32;
then A15: (G2 * (i,j)) `2 = (G2 * (1,j)) `2 by A13, A14, GOBOARD5:1
.= (G2 * (i2,j)) `2 by A5, A13, A14, GOBOARD5:1 ;
then A16: (G2 * (i2,j)) `2 < (G2 * (i2,j2)) `2 by A2, A4, A8, A9, A10, A11, GOBOARD5:4;
A17: now :: thesis: not j2 <= j
assume j2 <= j ; :: thesis: contradiction
then ( j = j2 or j2 < j ) by XXREAL_0:1;
hence contradiction by A5, A6, A14, A16, GOBOARD5:4; :: thesis: verum
end;
1 <= j2 -' 1 by A6, NAT_D:49;
then j2 -' 1 < j2 by NAT_D:51;
then A18: j2 -' 1 < width G2 by A7, XXREAL_0:2;
assume A19: (G2 * (i2,(j2 -' 1))) `2 < (G1 * (i1,(j1 -' 1))) `2 ; :: thesis: contradiction
now :: thesis: not j <= j2 -' 1
assume j <= j2 -' 1 ; :: thesis: contradiction
then ( j2 -' 1 = j or j < j2 -' 1 ) by XXREAL_0:1;
hence contradiction by A5, A19, A11, A13, A15, A18, GOBOARD5:4; :: thesis: verum
end;
hence contradiction by A17, NAT_D:49; :: thesis: verum