for j, l being Nat holds
( l <= j or l = j + 1 or j + 2 <= l )