for i being Nat holds i,i + 1 are_coprime