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

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

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

hence k,n are_coprime by INT_2:def 3; :: thesis: verum

end;

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

then n divides k by NAT_D:def 5;
hence k,n are_coprime by A1, NAT_D:7; :: thesis: verum

end;

end;