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)
k <= k + k by NAT_1:11;
then A2: k < n by A1, XXREAL_0:2;
then A3: n - k > 0 by XREAL_1:50;
A4: k > 0 by A1;
n * k > (2 * k) * k by A4, A1, XREAL_1:68;
then 0 < (n * k) - ((2 * k) * k) by XREAL_1:50;
then (n * n) + 0 < (n * n) + ((((2 * n) * k) - (k * n)) - ((2 * k) * k)) by XREAL_1:6;
then n * n < (n + (2 * k)) * (n - k) ;
then A5: n / (n - k) < (n + (2 * k)) / n by A1, A3, XREAL_1:106;
(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 A5, A2, Lm1; :: thesis: verum