theorem SierpCorr2: :: NUMBER18:69

for a, b being non zero Nat st a,b are_coprime holds
for n being Nat st n > a * b holds
ex x, y being non zero Nat st n = (a * x) + (b * y)