V.L03 — Integer threshold

Integer threshold lemma: for a non-increasing sequence of non-negative integers satisfying a_{n+1} <= floor((1 - iota_tau) a_n), starting from a_0 = N, there exists finite n_0 <= N/iota_tau such that a_{n_0} = 0. Integer-valuedness forces exact termination.