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