Function lemma_first_zero_index_clear 

pub proof fn lemma_first_zero_index_clear(s: Seq<bool>, i: int)

requires

0 <= i < s.len(),

s[i],

ensures

first_zero_index(s.update(i, false))
    == if first_zero_index(s) <= i { first_zero_index(s) } else { i },

Clearing a true bit at i moves the first zero to min(first_zero_index(s), i).