let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies ex u, v being Nat st (a * u) - (b * v) = 1 )
assume a,b are_coprime ; :: thesis: ex u, v being Nat st (a * u) - (b * v) = 1
then A1: a gcd b = 1 ;
ex c, d being Nat st a gcd b = (a * c) - (b * d) by WSIERP_1:31;
hence ex u, v being Nat st (a * u) - (b * v) = 1 by A1; :: thesis: verum