let a, b be Nat; :: thesis: ( b > 0 & a,b ! are_coprime implies a,b are_coprime )
assume A1: ( b > 0 & a,b ! are_coprime ) ; :: thesis: a,b are_coprime

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

suppose a = 0 ; :: thesis: a,b are_coprime

then b <= 1 by A1, Th23;
then b < 1 + 1 by NAT_1:13;
then ( b = 1 or b = 0 ) by NAT_1:23;
hence a,b are_coprime by A1, NEWTON:51; :: thesis: verum

end;

suppose a > 0 ; :: thesis: a,b are_coprime

hence a,b are_coprime by A1, Lm4; :: thesis: verum

end;

end;