let k, n be Nat; :: thesis: ( k <> 0 & k < n & n is prime implies k,n are_relative_prime )
assume A1: ( k <> 0 & k < n & n is prime ) ; :: thesis: k,n are_relative_prime
A2: k gcd n divides n by NAT_D:def 5;

per cases ( k gcd n = 1 or k gcd n = n ) by A1, A2, INT_2:def 5;

suppose k gcd n = 1 ; :: thesis: k,n are_relative_prime

hence k,n are_relative_prime by INT_2:def 4; :: thesis: verum

end;

suppose k gcd n = n ; :: thesis: k,n are_relative_prime

then A3: n divides k by NAT_D:def 5;
thus k,n are_relative_prime by A1, A3, NAT_D:7; :: thesis: verum

end;

end;