for i, k, l being Nat st i >= k + l holds
i >= k