let a, m, n be Nat; :: thesis: ( a,m are_coprime & n divides a implies n,m are_coprime )
assume A1: ( a,m are_coprime & n divides a ) ; :: thesis: n,m are_coprime
assume not n,m are_coprime ; :: thesis: contradiction
then consider k being Nat such that
A2: ( k divides n & k divides m & k <> 1 ) by PYTHTRIP:def 1;
k divides a by A1, A2, INT_2:9;
then k divides a gcd m by A2, INT_2:def 2;
hence contradiction by A2, A1, WSIERP_1:15; :: thesis: verum