for i1, j1 being Integer st i1,j1 are_coprime holds
ex s, t being Integer st (s * i1) + (t * j1) = 1