let n be Nat; :: thesis: ( n,n are_coprime iff n = 1 )

n gcd n = n by NAT_D:32;

hence ( n,n are_coprime iff n = 1 ) by INT_2:def 3; :: thesis: verum

n gcd n = n by NAT_D:32;

hence ( n,n are_coprime iff n = 1 ) by INT_2:def 3; :: thesis: verum