theorem LMThFRat31X: :: ZMODUL07:1
for n being Integer st n <> 0 & n <> - 1 & n <> - 2 holds
not n / (n + 1) in INT