let x, n be real number ; :: thesis: ( n >= 2 & x = 1 / (n + 1) implies x / (1 - x) < 1 )
A1: n + 1 > n by XREAL_1:31;
assume A2: ( n >= 2 & x = 1 / (n + 1) ) ; :: thesis: x / (1 - x) < 1
then A3: x > 0 ;
2 < n + 1 by A1, A2, XXREAL_0:2;
then 2 / (n + 1) < 1 by XREAL_1:191;
then 2 * x < 1 by A2;
then x + x < 1 ;
then x < 1 - x by XREAL_1:22;
hence x / (1 - x) < 1 by A3, XREAL_1:191; :: thesis: verum