for a, b being Nat st 1 < a holds
b < a |^ b