let a, b, c, d be Nat; :: thesis: ( a,c are_coprime & b,d are_coprime & a * b = c * d implies ( a = d & b = c ) )
assume A1: ( a,c are_coprime & b,d are_coprime ) ; :: thesis: ( not a * b = c * d or ( a = d & b = c ) )
assume A3: a * b = c * d ; :: thesis: ( a = d & b = c )

per cases ( a = 0 or not a = 0 ) ;

suppose a = 0 ; :: thesis: ( a = d & b = c )

then reconsider a = a as zero Nat ;
B2: a gcd c = 1 by A1;
c * d = a * b by A3
.= 0 ;
then reconsider d = d as zero Nat by B2;
d gcd b = 1 by A1;
then b = 1 ;
hence ( a = d & b = c ) by A3, B2; :: thesis: verum

end;

suppose not a = 0 ; :: thesis: ( a = d & b = c )

then reconsider a = a as non zero Nat ;
a divides c * d by A3;
then B1: a divides d by A1, INT_2:25;
d divides a * b by A3;
then B2: d divides a by A1, INT_2:25;
B3: not a = - d ;
then a * b = a * c by A3, B1, B2, INT_2:11;
hence ( a = d & b = c ) by B1, B2, B3, INT_2:11, XCMPLX_1:5; :: thesis: verum

end;

end;