let n, k be Nat; :: thesis: ( 0 < 2 * k & 2 * k <= n implies 1 / (1 - (k / n)) <= 1 + ((2 * k) / n) )
assume A1: ( 0 < 2 * k & 2 * k <= n ) ; :: thesis: 1 / (1 - (k / n)) <= 1 + ((2 * k) / n)
then k + k > 0 + k by XREAL_1:8;
then A2: n > k by A1, XXREAL_0:2;
A3: n - k > 0 by A2, XREAL_1:50;
n * k >= (2 * k) * k by A1, XREAL_1:64;
then 0 <= (n * k) - ((2 * k) * k) by XREAL_1:48;
then (n * n) + 0 <= (n * n) + ((((2 * n) * k) - (k * n)) - ((2 * k) * k)) by XREAL_1:7;
then n * n <= (n + (2 * k)) * (n - k) ;
then A4: n / (n - k) <= (n + (2 * k)) / n by A1, A3, XREAL_1:102;
(n + (2 * k)) / n = (n / n) + ((2 * k) / n) by XCMPLX_1:62
.= 1 + ((2 * k) / n) by A1, XCMPLX_1:60 ;
hence 1 / (1 - (k / n)) <= 1 + ((2 * k) / n) by A4, A2, Lm4; :: thesis: verum