let a, b be square Nat; :: thesis: ( (a + b) / 2 is square implies a mod 3 = b mod 3 )
assume (a + b) / 2 is square ; :: thesis: a mod 3 = b mod 3
then reconsider s = (a + b) / 2 as square Nat ;
A2: (a + b) mod 3 = (2 * s) mod 3
.= ((2 mod (2 + 1)) * (s mod 3)) mod 3 by NAT_D:67
.= (2 * (s mod 3)) mod 3 ;
A3: ( a mod 3 is trivial & b mod 3 is trivial & s mod 3 is trivial ) by SM3;

per cases then ( s mod 3 = 1 or s mod 3 = 0 ) by NAT_2:def 1;

suppose s mod 3 = 1 ; :: thesis: a mod 3 = b mod 3

then B2: 2 mod (2 + 1) = ((a mod 3) + (b mod 3)) mod 3 by A2, NAT_D:66;

per cases ( a mod 3 = 0 or a mod 3 = 1 ) by A3, NAT_2:def 1;

suppose a mod 3 = 0 ; :: thesis: a mod 3 = b mod 3

then not ((a mod 3) + (b mod 3)) mod 3 = 2 by A3;
hence a mod 3 = b mod 3 by B2; :: thesis: verum

end;

suppose C1: a mod 3 = 1 ; :: thesis: a mod 3 = b mod 3

per cases ( b mod 3 = 0 or b mod 3 = 1 ) by A3, NAT_2:def 1;

suppose b mod 3 = 0 ; :: thesis: a mod 3 = b mod 3

hence a mod 3 = b mod 3 by C1, B2; :: thesis: verum

end;

suppose b mod 3 = 1 ; :: thesis: a mod 3 = b mod 3

hence a mod 3 = b mod 3 by C1; :: thesis: verum

end;

end;

end;

end;

end;

suppose B1: s mod 3 = 0 ; :: thesis: a mod 3 = b mod 3

B3: ( a mod 3 = 1 & b mod 3 = 1 implies ((a mod 3) + (b mod 3)) mod 3 = 2 mod (2 + 1) ) ;
B4: ( a mod 3 = 1 & b mod 3 = 0 implies ((a mod 3) + (b mod 3)) mod 3 = 1 mod (1 + 2) ) ;
( a mod 3 = 0 & b mod 3 = 1 implies ((a mod 3) + (b mod 3)) mod 3 = 1 mod (1 + 2) ) ;
then ( a mod 3 = 0 & b mod 3 = 0 ) by B1, A2, NAT_D:66, B3, B4, A3, NAT_2:def 1;
hence a mod 3 = b mod 3 ; :: thesis: verum

end;

end;