let a, b, c be Nat; :: thesis: ( not a divides b implies not a * c divides b )
a divides a * c ;
hence ( not a divides b implies not a * c divides b ) by INT_2:9; :: thesis: verum