let a, b be odd square Nat; :: thesis: ( a,b are_coprime implies not 3 divides (a + b) / 2 )
assume A1: a,b are_coprime ; :: thesis: not 3 divides (a + b) / 2
((a + b) / 2) * 2 = a + b ;
then (a + b) / 2 divides a + b ;
hence not 3 divides (a + b) / 2 by A1, N02193, INT_2:9; :: thesis: verum