let n, k be Nat; :: thesis: ( k < n implies ( 1 - (k / n) = (n - k) / n & 1 / (1 - (k / n)) = n / (n - k) ) )
assume k < n ; :: thesis: ( 1 - (k / n) = (n - k) / n & 1 / (1 - (k / n)) = n / (n - k) )
then 1 - (k / n) = (n / n) - (k / n) by XCMPLX_1:60
.= (n - k) / n by XCMPLX_1:120 ;
hence ( 1 - (k / n) = (n - k) / n & 1 / (1 - (k / n)) = n / (n - k) ) by XCMPLX_1:57; :: thesis: verum