Function lemma_first_zero_index_advance_after_set 

pub proof fn lemma_first_zero_index_advance_after_set(s: Seq<bool>, k: int)

requires

0 < k <= s.len(),

is_first_zero(s, k - 1),

ensures

first_zero_index(s.update(k - 1, true)) == k + first_zero_index(s[k..]),

Setting the bit at k - 1 (the current first zero) to true, when the prefix [0, k - 1) is all true, advances the first zero to k + first_zero_index(s[k..]).