let a, b be Nat; :: thesis: ( ( a <> 0 or b <> 0 ) implies ex A, B being Nat st
( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime ) )
set d = a gcd b;
assume A1: ( a <> 0 or b <> 0 ) ; :: thesis: ex A, B being Nat st
( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime )
then consider A, B being Integer such that
A2: ( a = (a gcd b) * A & b = (a gcd b) * B ) and
A3: A,B are_coprime by INT_2:23;
( 0 <= A & 0 <= B ) by A1, A2;
then reconsider A = A, B = B as Element of NAT by INT_1:3;
take A ; :: thesis: ex B being Nat st
( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime )
take B ; :: thesis: ( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime )
thus ( a = (a gcd b) * A & b = (a gcd b) * B & A,B are_coprime ) by A2, A3; :: thesis: verum