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

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