Function lemma_first_zero_index_set_after_first_zero 

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

requires

0 <= i < s.len(),

first_zero_index(s) < i,

!s[i],

ensures

first_zero_index(s.update(i, true)) == first_zero_index(s),

Setting a false bit at i that is strictly past the first zero leaves the first zero unchanged.