Function lemma_first_zero_index_clear_range 

pub proof fn lemma_first_zero_index_clear_range(
    s: Seq<bool>,
    t: Seq<bool>,
    start: int,
    end: int,
)

requires

s.len() == t.len(),

0 <= start < end <= s.len(),

forall |j: int| 0 <= j < start ==> t[j] == s[j],

forall |j: int| start <= j < end ==> !t[j],

forall |j: int| end <= j < s.len() ==> t[j] == s[j],

ensures

first_zero_index(t)
    == if first_zero_index(s) <= start { first_zero_index(s) } else { start },

Clearing all bits in [start, end) moves the first zero to min(first_zero_index(s), start).