let a, b be Element of NAT ; :: thesis: ( not a,b are_coprime or a > 0 or b > 0 )
assume a,b are_coprime ; :: thesis: ( a > 0 or b > 0 )
then ( a is odd or b is odd ) by PYTHTRIP:10;
hence ( a > 0 or b > 0 ) by ABIAN:12; :: thesis: verum