let a, b be Integer; :: thesis: ( a <> b implies { n where n is Nat : a + n,b + n are_coprime } is infinite )
assume a <> b ; :: thesis: { n where n is Nat : a + n,b + n are_coprime } is infinite
then ( a < b or b < a ) by XXREAL_0:1;
hence { n where n is Nat : a + n,b + n are_coprime } is infinite by Lm39; :: thesis: verum