theorem SierpTh16: :: NUMBER18:67

for a, b being non zero Nat st a,b are_coprime holds
ex u, v being Nat st (a * u) - (b * v) = 1