let a, b be odd Nat; :: thesis: ( a - b = 2 implies a,b are_coprime )
assume A1: a - b = 2 ; :: thesis: a,b are_coprime
assume not a,b are_coprime ; :: thesis: contradiction
then consider k being Nat such that
A2: ( k divides a & k divides b ) and
A3: k <> 1 by PYTHTRIP:def 1;
k <= 2 by A1, A2, INT_5:1, INT_2:27;
then not not k = 0 & ... & not k = 2 ;
hence contradiction by A2, A3; :: thesis: verum