for x, y, z being Nat holds
( ( x >= z & y = x choose z ) iff ex u, v, y1, y2, y3 being Nat st
( y1 = x |^ z & y2 = (u + 1) |^ x & y3 = u |^ z & u > y1 & v = [\(y2 / y3)/] & y,v are_congruent_mod u & y < u & x >= z ) )