let x, n be Real; :: thesis: ( n >= 2 & x = 1 / (n + 1) implies x / (1 - x) < 1 )
assume that
A1: n >= 2 and
A2: x = 1 / (n + 1) ; :: thesis: x / (1 - x) < 1
n + 1 > n by XREAL_1:29;
then 2 < n + 1 by A1, XXREAL_0:2;
then 2 / (n + 1) < 1 by XREAL_1:189;
then x + x < 1 by A2;
then x < 1 - x by XREAL_1:20;
hence x / (1 - x) < 1 by A1, A2, XREAL_1:189; :: thesis: verum