let a, b be square Nat; :: thesis: ( a,b are_coprime & (a - b) / 2 is square implies b mod 3 = 1 )
assume A1: a,b are_coprime ; :: thesis: ( not (a - b) / 2 is square or b mod 3 = 1 )
assume (a - b) / 2 is square ; :: thesis: b mod 3 = 1
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;
A4: not 3 is trivial ;

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

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

then B2: 2 mod (2 + 1) = ((a mod 3) - (b mod 3)) mod 3 by A2, INT_6:7;

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

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

max ((a mod 3),(b mod 3)) > 0 by A1, A4, COM;
then not b mod 3 = 0 by C1;
hence b mod 3 = 1 by A3, NAT_2:def 1; :: thesis: verum

end;

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

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

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

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

end;

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

hence b mod 3 = 1 ; :: thesis: verum

end;

end;

end;

end;

end;

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

2 * s,b * 1 are_coprime by NEWTON02:5, A1;
then max ((b mod 3),(s mod 3)) > 0 by NEWTON01:41, A4, COM;
then b mod 3 > 0 by B1;
hence b mod 3 = 1 by A3, NAT_2:def 1; :: thesis: verum

end;

end;