let a, b, c be Nat; :: thesis: ( b <> 0 & b divides c & a * b,c are_coprime implies b = 1 )
assume b <> 0 ; :: thesis: ( not b divides c or not a * b,c are_coprime or b = 1 )
assume A1: b divides c ; :: thesis: ( not a * b,c are_coprime or b = 1 )
assume A2: a * b,c are_coprime ; :: thesis: b = 1
b divides a * b by INT_1:def 3;
then b divides (a * b) gcd c by A1, INT_2:22;
then b divides 1 by A2, INT_2:def 3;
hence b = 1 by INT_2:13; :: thesis: verum