let a, b be Integer; :: thesis: ( a,b are_coprime implies min ((Parity (a - b)),(Parity (a + b))) <= 2 )
assume A1: a,b are_coprime ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

per cases ( a is even or b is even or ( a is odd & b is odd ) ) ;

suppose B1: a is even ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

then b is odd by A1, PYTHTRIP10;
then ( Parity (a + b) = 1 & Parity (a - b) = 1 ) by B1, NAT_2:def 1;
hence min ((Parity (a - b)),(Parity (a + b))) <= 2 ; :: thesis: verum

end;

suppose B1: b is even ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

then a is odd by A1, PYTHTRIP10;
then ( Parity (a + b) = 1 & Parity (a - b) = 1 ) by B1, NAT_2:def 1;
hence min ((Parity (a - b)),(Parity (a + b))) <= 2 ; :: thesis: verum

end;

suppose ( a is odd & b is odd ) ; :: thesis: min ((Parity (a - b)),(Parity (a + b))) <= 2

hence min ((Parity (a - b)),(Parity (a + b))) <= 2 by ODP; :: thesis: verum

end;

end;