let a, m, n be Nat; :: thesis: ( m,n are_coprime implies (a * n) + m,n are_coprime )
(a * n) + m,m are_congruent_mod n ;
hence ( m,n are_coprime implies (a * n) + m,n are_coprime ) by WSIERP_1:43; :: thesis: verum