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;

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;

end;